Theorem equsexv

An equivalence related to implicit substitution. Version of equsex with a disjoint variable condition, which does not require [ax-13]. See equsexvw for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) Avoid [ax-10]. (Revised by GG, 18-Nov-2024.)

Hypotheses
equsalv.nf
\( \vdash \Finv x \, \psi \)
equsalv.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists x \, (x = y' \wedge \varphi) \leftrightarrow \psi \)
Proof
l0
equsalv.nf
equsalv.1
biimpa _
l3
exlimi l0 _
l4
equsalv.nf
equsalv.1
l6
equsalv l4 _
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \psi \)
equs4v
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow \exists x \, (x = y' \wedge \varphi) \)
sylbir l6 _
impbii l3 _