Theorem equvinva

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

	Ref	Expression
Assertion	equvinva	$$⊢x=y\to \exists z\left(x=z\wedge y=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax6evr	$$⊢\exists zy=z$$
2		equtr	$$⊢x=y\to \left(y=z\to x=z\right)$$
3	2	ancrd	$$⊢x=y\to \left(y=z\to \left(x=z\wedge y=z\right)\right)$$
4	3	eximdv	$$⊢x=y\to \left(\exists zy=z\to \exists z\left(x=z\wedge y=z\right)\right)$$
5	1 4	mpi	$$⊢x=y\to \exists z\left(x=z\wedge y=z\right)$$