Nuprl Lemma : eq_atom_wf1

[x,y:Atom1].  (x =a1 y ∈ 𝔹)


Proof




Definitions occuring in Statement :  eq_atom: eq_atom$n(x;y) atom: Atom$n bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T eq_atom: eq_atom$n(x;y)
Lemmas referenced :  btrue_wf bfalse_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut atomn_eqEquality hypothesisEquality extract_by_obid hypothesis sqequalHypSubstitution sqequalRule axiomEquality equalityTransitivity equalitySymmetry atomnEquality isect_memberEquality isectElimination thin because_Cache

Latex:
\mforall{}[x,y:Atom1].    (x  =a1  y  \mmember{}  \mBbbB{})



Date html generated: 2019_06_20-AM-11_20_14
Last ObjectModification: 2018_08_08-AM-10_56_01

Theory : atom_1


Home Index