Metamath Proof Explorer

Theorem wl-naevhba1v

Description: An instance of hbn1w applied to equality. (Contributed by Wolf Lammen, 7-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 equequ1 
 |-  ( x = z -> ( x = y <-> z = y ) )
2 1 hbn1w 
 |-  ( -. A. x x = y -> A. x -. A. x x = y )