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

Metamath Proof Explorer

Theorem equvinv

Description: A variable introduction law for equality. Lemma 15 of Monk2 p. 109. (Contributed by NM, 9-Jan-1993) Remove dependencies on ax-10 , ax-13 . (Revised by Wolf Lammen, 10-Jun-2019) Move the quantified variable ( z ) to the left of the equality signs. (Revised by Wolf Lammen, 11-Apr-2021) (Proof shortened by Wolf Lammen, 12-Jul-2022)

		Ref	Expression
	Assertion	equvinv	$⊢ x = y \leftrightarrow \exists z (z = x \land z = y)$

Proof

Step	Hyp	Ref	Expression
1		equequ1	$⊢ z = x \to (z = y \leftrightarrow x = y)$
2	1	equsexvw	$⊢ \exists z (z = x \land z = y) \leftrightarrow x = y$
3	2	bicomi	$⊢ x = y \leftrightarrow \exists z (z = x \land z = y)$