Theorem equs4

Lemma used in proofs of implicit substitution properties. The converse requires either a disjoint variable condition ( sbalex) or a nonfreeness hypothesis ( equs45f ). Usage of this theorem is discouraged because it depends on [ax-13]. See equs4v for a weaker version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow \exists x \, (x = y' \wedge \varphi) \)
Proof
l0
ax6e
\( \vdash \exists x \, x = y' \)
exintr
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow \exists x \, x = y' \rightarrow \exists x \, (x = y' \wedge \varphi) \)
mpi l0 _