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 ¬xx=yx¬xx=y

Proof

Step Hyp Ref Expression
1 equequ1 x=zx=yz=y
2 1 hbn1w ¬xx=yx¬xx=y