---

Step * of Lemma req*_functionality

∀[x1,x2,y1,y2:ℝ*].  (x1 = x2 ⇒ y1 = y2 ⇒ (x1 = y1 ⇐⇒ x2 = y2))
BY
{ Auto }

1
1. [x1] : ℝ*
2. [x2] : ℝ*
3. [y1] : ℝ*
4. [y2] : ℝ*
5. x1 = x2
6. y1 = y2
7. x1 = y1
⊢ x2 = y2

2
1. [x1] : ℝ*
2. [x2] : ℝ*
3. [y1] : ℝ*
4. [y2] : ℝ*
5. x1 = x2
6. y1 = y2
7. x2 = y2
⊢ x1 = y1

---

Latex:

---

Latex:
\mforall{}[x1,x2,y1,y2:\mBbbR{}*].    (x1  =  x2  {}\mRightarrow{}  y1  =  y2  {}\mRightarrow{}  (x1  =  y1  \mLeftarrow{}{}\mRightarrow{}  x2  =  y2))


By

---

Latex:
Auto

---

Home Index