Step * of Lemma classical-all

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

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

2
1. Type
2. T ⟶ ℙ
3. {∀x:T. {P[x]}}@i
4. 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