Theorem equs4v

Version of equs4 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-May-1993.) (Revised by BJ, 31-May-2019.)

Conclusion
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow \exists x \, (x = y' \wedge \varphi) \)
Proof
l0
ax6ev
\( \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 _