Theorem equvinva

A modified version of the forward implication of equvinv adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.)

Conclusion
\( \vdash x' = y' \rightarrow \exists z \, (x' = z \wedge y' = z) \)
Proof
l0
ax6evr
\( \vdash \exists z \, y' = z \)
equtr
ancrd _
eximdv _
\( \vdash x' = y' \rightarrow \exists z \, y' = z \rightarrow \exists z \, (x' = z \wedge y' = z) \)
mpi l0 _