---

Step * of Lemma neg_assert_of_eq_atom1

∀[x,y:Atom1].  uiff(¬↑x =a1 y;x ≠ y ∈ Atom1 )
BY
{ UnivCD
THENM RWH (LemmaC `assert_of_eq_atom1`) 0
THENA Auto⋅⋅ }

1
1. x : Atom1
2. y : Atom1
⊢ uiff(¬(x = y ∈ Atom1);x ≠ y ∈ Atom1 )

---

Latex:

---

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


By

---

Latex:
UnivCD
THENM  RWH  (LemmaC  `assert\_of\_eq\_atom1`)  0
THENA  Auto\mcdot{}\mcdot{}

---

Home Index