---

Step * of Lemma sub-equality

∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[i,u:T].  (i = u ∈ {j:T| {j:T| P j} } ) supposing ((P u) and (i = u ∈ T))
BY
{ Auto }

1
1. T : Type
2. P : T ⟶ ℙ
3. i : T
4. u : T
5. i = u ∈ T
6. P u
⊢ i = u ∈ {j:T| {j:T| P j} } 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[i,u:T].    (i  =  u)  supposing  ((P  u)  and  (i  =  u))


By

---

Latex:
Auto

---

Home Index