Theorem equsexALT

Alternate proof of equsex. This proves the result directly, instead of as a corollary of equsal via equs4. Note in particular that only existential quantifiers appear in the proof and that the only step requiring [ax-13] is ax6e. This proof mimics that of equsal (in particular, note that pm5.32i, exbii, 19.41, mpbiran correspond respectively to pm5.74i, albii, 19.23, a1bi ). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (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
equsal.2
pm5.32i _
l2
exbii _
\( \vdash \exists x \, (x = y' \wedge \varphi) \leftrightarrow \exists x \, (x = y' \wedge \psi) \)
l3
ax6e
\( \vdash \exists x \, x = y' \)
equsal.1
19.41 _
\( \vdash \exists x \, (x = y' \wedge \psi) \leftrightarrow \exists x \, x = y' \wedge \psi \)
mpbiran l3 _
\( \vdash \exists x \, (x = y' \wedge \psi) \leftrightarrow \psi \)
bitri l2 _