Theorem equsal

An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. See equsalvw and equsalv for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (New usage is discouraged.)

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