---

Step * 1 1 of Lemma implies-quotient-true2


1. P : ℙ
2. Q : ℙ
3. P ⇒ ⇃(Q)
4. ⇃(P)
5. x : ⇃(⇃(Q))
⊢ x ∈ ⇃(Q)
BY
{ (Unfold `member` 0 THEN QuotientElimForEquality (-1)⋅ THEN GenConclTerms Auto [⌜x⌝;⌜x1⌝]⋅ THEN All Thin) }

1
1. Q : ℙ
2. v : ⇃(Q)
3. v1 : ⇃(Q)
⊢ v = v1 ∈ ⇃(Q)

---

Latex:

---

Latex:

1.  P  :  \mBbbP{}
2.  Q  :  \mBbbP{}
3.  P  {}\mRightarrow{}  \00D9(Q)
4.  \00D9(P)
5.  x  :  \00D9(\00D9(Q))
\mvdash{}  x  \mmember{}  \00D9(Q)


By

---

Latex:
(Unfold  `member`  0
  THEN  QuotientElimForEquality
  (-1)\mcdot{}
  THEN  GenConclTerms  Auto  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index