Theorem equsexhv

An equivalence related to implicit substitution. Version of equsexh with a disjoint variable condition, which does not require [ax-13]. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.)

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