---

Step * 1 of Lemma equipollent-set


1. [T] : Type
2. [P] : T ⟶ ℙ
3. b : {x:T| ↓P[x]} 
⊢ ∃a:{x:T| P[x]} . (a = b ∈ {x:T| ↓P[x]} )
BY
{ (D -1 THEN InstConcl [⌜b⌝]⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  b  :  \{x:T|  \mdownarrow{}P[x]\} 
\mvdash{}  \mexists{}a:\{x:T|  P[x]\}  .  (a  =  b)


By

---

Latex:
(D  -1  THEN  InstConcl  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index