---

Step * 1 1 1 of Lemma implies-quotient-true2


1. Q : ℙ
2. v : ⇃(Q)
3. v1 : ⇃(Q)
⊢ v = v1 ∈ ⇃(Q)
BY
{ (QuotientElimForEquality (-2) THEN QuotientElimForEquality (-1))⋅ }

1
1. Q : ℙ
2. v : Base
3. v2 : Base
4. v = v2 ∈ pertype(λx,y. ((x ∈ Q) ∧ (y ∈ Q) ∧ True))
5. v ∈ Q
6. v2 ∈ Q
7. True
8. v1 : Base
9. v3 : Base
10. v1 = v3 ∈ pertype(λx,y. ((x ∈ Q) ∧ (y ∈ Q) ∧ True))
11. v1 ∈ Q
12. v3 ∈ Q
13. True
⊢ v = v3 ∈ ⇃(Q)

---

Latex:

---

Latex:

1.  Q  :  \mBbbP{}
2.  v  :  \00D9(Q)
3.  v1  :  \00D9(Q)
\mvdash{}  v  =  v1


By

---

Latex:
(QuotientElimForEquality  (-2)  THEN  QuotientElimForEquality  (-1))\mcdot{}

---

Home Index