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 z z = x z = y

Proof

Step Hyp Ref Expression
1 equequ1 z = x z = y x = y
2 1 equsexvw z z = x z = y x = y
3 2 bicomi x = y z z = x z = y