Nuprl Lemma : equal_wf

[A:Type]. ∀[a,b:A].  (a b ∈ A ∈ ℙ)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: member: t ∈ T universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] prop: member: t ∈ T
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation because_Cache hypothesisEquality universeEquality equalityEquality

Latex:
\mforall{}[A:Type].  \mforall{}[a,b:A].    (a  =  b  \mmember{}  \mBbbP{})



Date html generated: 2018_05_21-PM-00_00_01
Last ObjectModification: 2017_11_03-PM-10_11_48

Theory : core_2


Home Index