Theorem equsexvw

Version of equsexv with a disjoint variable condition, and of equsex with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw. (Contributed by BJ, 31-May-2019.) (Proof shortened by Wolf Lammen, 23-Oct-2023.)

Hypothesis
equsalvw.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists x \, (x = y' \wedge \varphi) \leftrightarrow \psi \)
Proof
l0
alinexa
\( \vdash \forall x \, (x = y' \rightarrow \neg \varphi) \leftrightarrow \neg \exists x \, (x = y' \wedge \varphi) \)
equsalvw.1
notbid _
equsalvw _
\( \vdash \forall x \, (x = y' \rightarrow \neg \varphi) \leftrightarrow \neg \psi \)
bitr3i l0 _
con4bii _