Theorem equsalvw

Version of equsalv with a disjoint variable condition, and of equsal with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw. (Contributed by BJ, 31-May-2019.)

Hypothesis
equsalvw.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \psi \)
Proof
equsalvw.1
pm5.74i _
l2
albii _
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \forall x \, (x = y' \rightarrow \psi) \)
equsv
\( \vdash \forall x \, (x = y' \rightarrow \psi) \leftrightarrow \psi \)
bitri l2 _