Theorem ax6evr

A commuted form of ax6ev. (Contributed by BJ, 7-Dec-2020.)

Conclusion
\( \vdash \exists x \, y' = x \)
Proof
l0
ax6ev
\( \vdash \exists x \, x = y' \)
equcomiv
\( \vdash x = y' \rightarrow y' = x \)
eximii l0 _