---

Step * of Lemma trivial-mFOL-rename

∀x,y:ℤ. ∀fmla:mFOL().  ((¬(y ∈ mFOL-freevars(fmla))) ⇒ (fmla = mFOL-rename(fmla;y;x) ∈ mFOL()))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. x : ℤ
2. y : ℤ
⊢ ∀fmla:mFOL(). ((¬(y ∈ mFOL-freevars(fmla))) ⇒ (fmla = mFOL-rename(fmla;y;x) ∈ mFOL()))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.  \mforall{}fmla:mFOL().    ((\mneg{}(y  \mmember{}  mFOL-freevars(fmla)))  {}\mRightarrow{}  (fmla  =  mFOL-rename(fmla;y;x)))


By

---

Latex:
RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index