---

Step * of Lemma FormExists_wf2

∀[C:Type]. ∀[a:PZF-Formula(C)]. ∀[x:Atom].  (∃x. a ∈ PZF-Formula(C))
BY
{ (Auto THEN RepeatFor 2 (D 2) THEN RepeatFor 2 ((MemTypeCD THEN Auto))) }

1
1. C : Type
2. a : Form(C)
3. ↑wfForm(a)
4. ↑SafeForm(a)
5. ¬↑termForm(a)
6. x : Atom
⊢ ↑wfForm(∃x. a)

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[a:PZF-Formula(C)].  \mforall{}[x:Atom].    (\mexists{}x.  a  \mmember{}  PZF-Formula(C))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  2)  THEN  RepeatFor  2  ((MemTypeCD  THEN  Auto)))

---

Home Index