Theorem equsalhw

Version of equsalh with a disjoint variable condition, which does not require [ax-13]. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)

Hypotheses
equsalhw.1
\( \vdash \psi \rightarrow \forall x \, \psi \)
equsalhw.2
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \psi \)
Proof
equsalhw.1
l1
nf5i _
equsalhw.2
equsalv l1 _