Step * of Lemma classical-exists2

[T:Type]. ∀[P:T ⟶ ℙ].  uiff(¬(∀x:T. P[x]));{∃x:T. P[x]})
BY
Auto }

1
1. Type
2. T ⟶ ℙ
3. ¬(∀x:T. P[x]))
⊢ {∃x:T. P[x]}

2
1. Type
2. T ⟶ ℙ
3. {∃x:T. P[x]}
⊢ ¬(∀x:T. P[x]))


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    uiff(\mneg{}(\mforall{}x:T.  (\mneg{}P[x]));\{\mexists{}x:T.  P[x]\})


By


Latex:
Auto




Home Index