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	|- E. x A. y -. y e. x

Proof

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