---

Step * of Lemma req-iff-rsub-is-0

∀[a,b:ℝ].  uiff(a = b;(a - b) = r0)
BY
{ Auto }

1
1. a : ℝ
2. b : ℝ
3. a = b
⊢ (a - b) = r0

2
1. a : ℝ
2. b : ℝ
3. (a - b) = r0
⊢ a = b

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].    uiff(a  =  b;(a  -  b)  =  r0)


By

---

Latex:
Auto

---

Home Index