---

Step * of Lemma equiv_rel_iff

EquivRel(ℙ;A,B.A ⇐⇒ B)
BY
{ Unfold `equiv_rel` 0 }

1
Refl(ℙ;A,B.A ⇐⇒ B) ∧ Sym(ℙ;A,B.A ⇐⇒ B) ∧ Trans(ℙ;A,B.A ⇐⇒ B)

---

Latex:

---

Latex:
EquivRel(\mBbbP{};A,B.A  \mLeftarrow{}{}\mRightarrow{}  B)


By

---

Latex:
Unfold  `equiv\_rel`  0

---

Home Index