---

Step * 1 of Lemma neg_assert_of_eq_atom1


1. x : Atom1
2. y : Atom1
⊢ uiff(¬(x = y ∈ Atom1);x ≠ y ∈ Atom1 )
BY
{ Unfold `nequal` 0 THEN Auto⋅⋅ }

---

Latex:

---

Latex:

1.  x  :  Atom1
2.  y  :  Atom1
\mvdash{}  uiff(\mneg{}(x  =  y);x  \mneq{}  y  \mmember{}  Atom1  )


By

---

Latex:
Unfold  `nequal`  0  THEN  Auto\mcdot{}\mcdot{}

---

Home Index