Theorem equsv

If a formula does not contain a variable \( x \), then it is equivalent to the corresponding prototype of substitution with a fresh variable (see sb6 ). (Contributed by BJ, 23-Jul-2023.)

Conclusion
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \varphi \)
Proof
l0
19.23v
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \exists x \, x = y' \rightarrow \varphi \)
ax6ev
a1bi _
\( \vdash \varphi \leftrightarrow \exists x \, x = y' \rightarrow \varphi \)
bitr4i l0 _