Theorem equsexh

An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. See equsexhv for a version with a disjoint variable condition which does not require [ax-13]. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)

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