Metamath Proof Explorer


Theorem equvini

Description: A variable introduction law for equality. Lemma 15 of Monk2 p. 109, however we do not require z to be distinct from x and y . Usage of this theorem is discouraged because it depends on ax-13 . See equvinv for a shorter proof requiring fewer axioms when z is required to be distinct from x and y . (Contributed by NM, 10-Jan-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 16-Sep-2023) (New usage is discouraged.)

Ref Expression
Assertion equvini x=yzx=zz=y

Proof

Step Hyp Ref Expression
1 equtr z=xx=yz=y
2 equcomi z=xx=z
3 1 2 jctild z=xx=yx=zz=y
4 19.8a x=zz=yzx=zz=y
5 3 4 syl6 z=xx=yzx=zz=y
6 ax13 ¬z=xx=yzx=y
7 ax6e zz=x
8 7 3 eximii zx=yx=zz=y
9 8 19.35i zx=yzx=zz=y
10 6 9 syl6 ¬z=xx=yzx=zz=y
11 5 10 pm2.61i x=yzx=zz=y