Nuprl Lemma : neg_assert_of_eq_atom1

`∀[x,y:Atom1].  uiff(¬↑x =a1 y;x ≠ y ∈ Atom1 )`

Proof

Definitions occuring in Statement :  eq_atom: `eq_atom\$n(x;y)` atom: `Atom\$n` assert: `↑b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` nequal: `a ≠ b ∈ T ` not: `¬A`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` nequal: `a ≠ b ∈ T ` false: `False`
Lemmas referenced :  assert_of_eq_atom1 equal-wf-base atom1_subtype_base not_wf assert_wf eq_atom_wf1 nequal_wf uiff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut addLevel sqequalHypSubstitution productElimination thin independent_pairFormation independent_isectElimination lambdaFormation independent_functionElimination extract_by_obid isectElimination hypothesisEquality hypothesis atomnEquality applyEquality sqequalRule lambdaEquality dependent_functionElimination voidElimination instantiate cumulativity independent_pairEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[x,y:Atom1].    uiff(\mneg{}\muparrow{}x  =a1  y;x  \mneq{}  y  \mmember{}  Atom1  )

Date html generated: 2017_04_14-AM-07_14_35
Last ObjectModification: 2017_02_27-PM-02_50_15

Theory : atom_1

Home Index