---

Step * 1 of Lemma equiv_rel_iff


Refl(ℙ;A,B.A ⇐⇒ B) ∧ Sym(ℙ;A,B.A ⇐⇒ B) ∧ Trans(ℙ;A,B.A ⇐⇒ B)
BY
{ (((Unfolds ``refl sym trans`` 0 THEN GenUnivCD) THENM HypBackchain) THEN Auto) }

---

Latex:

---

Latex:

Refl(\mBbbP{};A,B.A  \mLeftarrow{}{}\mRightarrow{}  B)  \mwedge{}  Sym(\mBbbP{};A,B.A  \mLeftarrow{}{}\mRightarrow{}  B)  \mwedge{}  Trans(\mBbbP{};A,B.A  \mLeftarrow{}{}\mRightarrow{}  B)


By

---

Latex:
(((Unfolds  ``refl  sym  trans``  0  THEN  GenUnivCD)  THENM  HypBackchain)  THEN  Auto)

---

Home Index