---

Step * 1 1 1 of Lemma page55-again

.....antecedent..... 
1. U : Type@i'
2. P : U ⟶ ℙ@i'
3. Q : U ⟶ ℙ@i'
4. ∀x:U. (P x)@i
5. x : U@i
⊢ P x
BY
{ With x (D 4)⋅ }

1
.....wf..... 
1. U : Type@i'
2. P : U ⟶ ℙ@i'
3. Q : U ⟶ ℙ@i'
4. x : U@i
⊢ x ∈ U

2
1. U : Type@i'
2. P : U ⟶ ℙ@i'
3. Q : U ⟶ ℙ@i'
4. x : U@i
5. P x@i
⊢ P x

---

Latex:

---

Latex:
.....antecedent..... 
1.  U  :  Type@i'
2.  P  :  U  {}\mrightarrow{}  \mBbbP{}@i'
3.  Q  :  U  {}\mrightarrow{}  \mBbbP{}@i'
4.  \mforall{}x:U.  (P  x)@i
5.  x  :  U@i
\mvdash{}  P  x


By

---

Latex:
With  x  (D  4)\mcdot{}

---

Home Index