Is it true that "if $y$ is free for $x$ in a well-formed formula $\mathcal{B(x,x)}$, then $x$ is free for $y$ in $\mathcal{B(x,y)}$?" Two axiom schemas for first-order theories with equality are given in Mendelson's book "Introduction to Mathematical Logic (5th ed.)":
(A6) $(\forall x_1) x_1=x_1$ (reflexivity of equality)
(A7) $x=y\Rightarrow (\mathcal{B(x,x)}\Rightarrow \mathcal{B(x,y)})$ (substitutivity of equality)
where $x$ and $y$ are any variables, $\mathcal{B(x,x)}$ is a wf, and $\mathcal{B(x,y)}$ arises from $\mathcal{B(x,x)}$ by replacing some, but not necessarily all, free occurrences of $x$ by $y$,
with the proviso that $y$ is free for $x$ in $\mathcal{B(x,x)}$. Thus, $\mathcal{B(x,y)}$ may or may not
contain free occurrences of $x$.
Proposition 2.24 asserts that schema (A7) can be reduced to a few simpler cases as follows:
Proposition 2.24:
Let $K$ be a theory for which (A6) holds and (A7) holds for all atomic wfs (well-formed formulas)
$\mathcal{B(x,x)}$ in which there are no individual constants. Then $K$ is a theory with equality, that is, (A7) holds for all wfs $\mathcal{B(x,x)}$.
The proof of Proposition 2.24 is by induction on the number $n$ of connectives and quantifiers in $\mathcal{B(x,x)}$. After showing that (A7) holds for all atomic wfs $\mathcal{B(x,x)}$, the proof proceeds to the inductive step. In Case 1, i.e., $\mathcal{B(x,x)}=\neg\mathcal{C(x,x)}$, of the inductive step, it is asserted that $\vdash y=x\Rightarrow (\mathcal{C(x,y)}\Rightarrow \mathcal{C(x,x)})$ by inductive hypothesis. However, to apply the inductive hypothesis, we need "$x$ is free for $y$ in $\mathcal{C(x,y)}$" (not "$y$ is free for $x$ in $\mathcal{C(x,x)}$" that is at our disposal in this case).
So my question is: Is it true that if $y$ is free for $x$ in $\mathcal{B(x,x)}$, then $x$ is free for $y$ in $\mathcal{B(x,y)}$?" Or how to fix this proof of Proposition 2.24? Or my reasoning about the proof in Case 1 above is not correct.
Many thanks for any comments or hints.
 A: There is nothing to be fixed.
The induction step involving $\lnot$ uses the "reversed" axiom: $y = x \to (C(x,y) \to C(x,x))$ and the request is that $x$ is free for $y$ [see def. page 46] because we want to replace (one or more occurrences of) $y$ with $x$ into $C(x,y)$ to get $C(x,x)$.
In a nutshell, we want to avoid uncorrect substitutions like this one: $C(x,y) := Px \land \forall x (x < y)$ where the second occurrence of $x$ replacing $y$ will be "captured" by the $\forall x$ quantifier.
Having done this, the "propositional transformations" will produce: $x=y \to (\lnot C(x,x) \to \lnot C(x,y))$.
During these "transformational" steps there are no new substitutions to be performed. Thus, the proviso that $x$ must be free for $y$ is not used.

Having said that:

Is it true that "if $y$ is free for $x$ in a well-formed formula $\mathcal{B(x,x)}$, then $x$ is free for $y$ in $\mathcal{B(x,y)}$?"

The question must be better "specified": if $\mathcal{B(x,y)}$ is obtained from $\mathcal{B(x,x)}$ correctly replacing one (or more) occurrences of $x$ with $y$, can we reverse the operation and replace the newly introduced $y$ with $x$ to restore the original formula?
The answer is YES, because if the operation in correctly preformed the new $y$ in $\mathcal{B(x,y)}$ is not in the scope of a $\forall y$ quantifier and thus restoring $x$ does not produce any harm.
May it happens that the "restored" $x$ will be captured by a $\forall x$ quantifier?
NO, because if so this means that the newly introduced $y$ has replaced an $x$ that was in the scope of a $\forall x$ quantifier, and this type of substitution is not allowed.
