---

Step * 1 of Lemma sub-equality


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} } 
BY
{ (MemTypeCD THEN Auto) }

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbP{}
3.  i  :  T
4.  u  :  T
5.  i  =  u
6.  P  u
\mvdash{}  i  =  u


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index