---

Step * of Lemma mFOL-rename_wf

∀[fmla:mFOL()]. ∀[old,new:ℤ].  (mFOL-rename(fmla;old;new) ∈ mFOL())
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[fmla:mFOL()].  \mforall{}[old,new:\mBbbZ{}].    (mFOL-rename(fmla;old;new)  \mmember{}  mFOL())


By

ProveWfLemma

---

Home Index