Theorem equsalv

An equivalence related to implicit substitution. Version of equsal with a disjoint variable condition, which does not require [ax-13]. See equsalvw for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsexv. (Contributed by NM, 2-Jun-1993.) (Revised by BJ, 31-May-2019.)

Hypotheses
equsalv.nf
\( \vdash \Finv x \, \psi \)
equsalv.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \psi \)
Proof
equsalv.nf
l1
19.23 _
\( \vdash \forall x \, (x = y' \rightarrow \psi) \leftrightarrow \exists x \, x = y' \rightarrow \psi \)
equsalv.1
pm5.74i _
l4
albii _
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \forall x \, (x = y' \rightarrow \psi) \)
ax6ev
a1bi _
\( \vdash \psi \leftrightarrow \exists x \, x = y' \rightarrow \psi \)
3bitr4i l1 l4 _