Metamath Proof Explorer


Theorem wl-nfnae1

Description: Unlike nfnae , this specialized theorem avoids ax-11 . (Contributed by Wolf Lammen, 27-Jun-2019)

Ref Expression
Assertion wl-nfnae1 x¬yy=x

Proof

Step Hyp Ref Expression
1 wl-nfae1 xyy=x
2 1 nfn x¬yy=x