Metamath Proof Explorer


Theorem ax13dgen2

Description: Degenerate instance of ax-13 where bundled variables x and z have a common substitution. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 13-Apr-2017)

Ref Expression
Assertion ax13dgen2 ¬ x = y y = x x y = x

Proof

Step Hyp Ref Expression
1 equcomi y = x x = y
2 pm2.21 ¬ x = y x = y x y = x
3 1 2 syl5 ¬ x = y y = x x y = x