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

Proof

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