Theorem equsex

An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. See equsexvw and equsexv for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal. See equsexALT for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.) (New usage is discouraged.)

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