Metamath Proof Explorer


Theorem axc11n11

Description: Proof of axc11n from { ax-1 -- ax-7 , axc11 } . Almost identical to axc11nfromc11 . (Contributed by NM, 6-Jul-2021) (Proof modification is discouraged.)

Ref Expression
Assertion axc11n11
|- ( A. x x = y -> A. y y = x )

Proof

Step Hyp Ref Expression
1 axc11
 |-  ( A. x x = y -> ( A. x x = y -> A. y x = y ) )
2 1 pm2.43i
 |-  ( A. x x = y -> A. y x = y )
3 equcomi
 |-  ( x = y -> y = x )
4 2 3 sylg
 |-  ( A. x x = y -> A. y y = x )