This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (x = z \land y = z)$

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