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	$$⊢\exists x\forall y\neg y\in x$$

Proof

Step	Hyp	Ref	Expression
1		nfnae	$$⊢Ⅎy\neg \forall xx=y$$
2		nfcvf	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xy$$
3		nfcvd	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xz$$
4	2 3	nfeld	$$⊢\neg \forall xx=y\to Ⅎxy\in z$$
5	4	nfnd	$$⊢\neg \forall xx=y\to Ⅎx\neg y\in z$$
6	1 5	nfald	$$⊢\neg \forall xx=y\to Ⅎx\forall y\neg y\in z$$
7		nfvd	$$⊢\neg \forall xx=y\to Ⅎz\forall y\neg y\in x$$
8		dveeq2	$$⊢\neg \forall yy=x\to \left(z=x\to \forall yz=x\right)$$
9	8	naecoms	$$⊢\neg \forall xx=y\to \left(z=x\to \forall yz=x\right)$$
10		elequ2	$$⊢z=x\to \left(y\in z\leftrightarrow y\in x\right)$$
11	10	notbid	$$⊢z=x\to \left(\neg y\in z\leftrightarrow \neg y\in x\right)$$
12	11	biimpd	$$⊢z=x\to \left(\neg y\in z\to \neg y\in x\right)$$
13	12	al2imi	$$⊢\forall yz=x\to \left(\forall y\neg y\in z\to \forall y\neg y\in x\right)$$
14	9 13	syl6	$$⊢\neg \forall xx=y\to \left(z=x\to \left(\forall y\neg y\in z\to \forall y\neg y\in x\right)\right)$$
15		elequ1	$$⊢x=y\to \left(x\in x\leftrightarrow y\in x\right)$$
16	15	notbid	$$⊢x=y\to \left(\neg x\in x\leftrightarrow \neg y\in x\right)$$
17	16	sps	$$⊢\forall xx=y\to \left(\neg x\in x\leftrightarrow \neg y\in x\right)$$
18	17	dral1	$$⊢\forall xx=y\to \left(\forall x\neg x\in x\leftrightarrow \forall y\neg y\in x\right)$$
19	18	biimpd	$$⊢\forall xx=y\to \left(\forall x\neg x\in x\to \forall y\neg y\in x\right)$$
20		ax-nul	$$⊢\exists z\forall y\neg y\in z$$
21		elirrv	$$⊢\neg x\in x$$
22	21	ax-gen	$$⊢\forall x\neg x\in x$$
23	22	exgen	$$⊢\exists x\forall x\neg x\in x$$
24	6 7 14 19 20 23	dvelimexcasei	$$⊢\exists x\forall y\neg y\in x$$