---

Step * of Lemma rneq_functionality

∀x1,x2,y1,y2:ℝ.  (x1 ≠ y1 ⇐⇒ x2 ≠ y2) supposing ((y1 = y2) and (x1 = x2))
BY
{ ((UnivCD THENA Auto) THEN Unfold `rneq` 0 THEN ∀h:hyp. SubstReal h 0  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x1,x2,y1,y2:\mBbbR{}.    (x1  \mneq{}  y1  \mLeftarrow{}{}\mRightarrow{}  x2  \mneq{}  y2)  supposing  ((y1  =  y2)  and  (x1  =  x2))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `rneq`  0  THEN  \mforall{}h:hyp.  SubstReal  h  0    THEN  Auto)

---

Home Index