Theorem alequexv

Version of equs4v with its consequence simplified by exsimpr. (Contributed by BJ, 9-Nov-2021.)

Conclusion
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow \exists x \, \varphi \)
Proof
l0
ax6ev
\( \vdash \exists x \, x = y' \)
exim
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow \exists x \, x = y' \rightarrow \exists x \, \varphi \)
mpi l0 _