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 <-> E. z ( z = x /\ z = y ) )

Proof

Step	Hyp	Ref	Expression
1		equequ1	|- ( z = x -> ( z = y <-> x = y ) )
2	1	equsexvw	|- ( E. z ( z = x /\ z = y ) <-> x = y )
3	2	bicomi	|- ( x = y <-> E. z ( z = x /\ z = y ) )