---

Step * of Lemma not_over_exists_uniform

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

1
1. T : Type
2. Q : T ⟶ ℙ
3. ¬(∃x:T. Q[x])
4. x : T
⊢ ¬Q[x]

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

---

Latex:

---

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


By

---

Latex:
(GenRepD  THENA  Auto)

---

Home Index