Metamath Proof Explorer


Theorem axnulg

Description: A generalization of ax-nul in which x and y need not be distinct. Note that it is possible to use axc7e to derive elirrv from this theorem, which justifies the dependency on ax-reg . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 3-Aug-2025) (New usage is discouraged.)

Ref Expression
Assertion axnulg x y ¬ y x

Proof

Step Hyp Ref Expression
1 nfnae y ¬ x x = y
2 nfcvf ¬ x x = y _ x y
3 nfcvd ¬ x x = y _ x z
4 2 3 nfeld ¬ x x = y x y z
5 4 nfnd ¬ x x = y x ¬ y z
6 1 5 nfald ¬ x x = y x y ¬ y z
7 nfvd ¬ x x = y z y ¬ y x
8 dveeq2 ¬ y y = x z = x y z = x
9 8 naecoms ¬ x x = y z = x y z = x
10 elequ2 z = x y z y x
11 10 notbid z = x ¬ y z ¬ y x
12 11 biimpd z = x ¬ y z ¬ y x
13 12 al2imi y z = x y ¬ y z y ¬ y x
14 9 13 syl6 ¬ x x = y z = x y ¬ y z y ¬ y x
15 elequ1 x = y x x y x
16 15 notbid x = y ¬ x x ¬ y x
17 16 sps x x = y ¬ x x ¬ y x
18 17 dral1 x x = y x ¬ x x y ¬ y x
19 18 biimpd x x = y x ¬ x x y ¬ y x
20 ax-nul z y ¬ y z
21 elirrv ¬ x x
22 21 ax-gen x ¬ x x
23 22 exgen x x ¬ x x
24 6 7 14 19 20 23 dvelimexcasei x y ¬ y x