Theorem chvarfv

Implicit substitution of \( y' \) for \( x \) into a theorem. Version of chvar with a disjoint variable condition, which does not require [ax-13]. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)

Hypotheses
chvarfv.nf
\( \vdash \Finv x \, \psi \)
chvarfv.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
chvarfv.2
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \)
Proof
l0
chvarfv.nf
\( \vdash \Finv x \, \psi \)
chvarfv.1
biimpd _
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
l3
spimfv l0 _
\( \vdash \forall x \, \varphi \rightarrow \psi \)
chvarfv.2
\( \vdash \varphi \)
mpg l3 _