---

Step * of Lemma classical-all

∀[T:Type]. ∀[P:T ⟶ ℙ].  (∀x:T. {P[x]} ⇐⇒ {∀x:T. {P[x]}})
BY
{ Auto }

1
1. T : Type
2. P : T ⟶ ℙ
3. ∀x:T. {P[x]}@i
⊢ {∀x:T. {P[x]}}

2
1. T : Type
2. P : T ⟶ ℙ
3. {∀x:T. {P[x]}}@i
4. x : T@i
⊢ {P[x]}

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    (\mforall{}x:T.  \{P[x]\}  \mLeftarrow{}{}\mRightarrow{}  \{\mforall{}x:T.  \{P[x]\}\})


By

---

Latex:
Auto

---

Home Index