---

Step * of Lemma classical-exists2

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

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

2
1. T : Type
2. P : 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