Metamath Proof Explorer

Theorem wl-hbae1

Description: This specialization of hbae does not depend on ax-11 . (Contributed by Wolf Lammen, 8-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 axc11n 
 |-  ( A. x x = y -> A. y y = x )
2 axc11n 
 |-  ( A. y y = x -> A. x x = y )
3 2 axc4i 
 |-  ( A. y y = x -> A. y A. x x = y )
4 1 3 syl 
 |-  ( A. x x = y -> A. y A. x x = y )