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	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥

Proof

Step	Hyp	Ref	Expression
1		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
2		nfcvf	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
3		nfcvd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑧 )
4	2 3	nfeld	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 ∈ 𝑧 )
5	4	nfnd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ¬ 𝑦 ∈ 𝑧 )
6	1 5	nfald	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑧 )
7		nfvd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
8		dveeq2	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( 𝑧 = 𝑥 → ∀ 𝑦 𝑧 = 𝑥 ) )
9	8	naecoms	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑥 → ∀ 𝑦 𝑧 = 𝑥 ) )
10		elequ2	⊢ ( 𝑧 = 𝑥 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑥 ) )
11	10	notbid	⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑦 ∈ 𝑧 ↔ ¬ 𝑦 ∈ 𝑥 ) )
12	11	biimpd	⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑥 ) )
13	12	al2imi	⊢ ( ∀ 𝑦 𝑧 = 𝑥 → ( ∀ 𝑦 ¬ 𝑦 ∈ 𝑧 → ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) )
14	9 13	syl6	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑥 → ( ∀ 𝑦 ¬ 𝑦 ∈ 𝑧 → ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) ) )
15		elequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
16	15	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝑦 ∈ 𝑥 ) )
17	16	sps	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝑦 ∈ 𝑥 ) )
18	17	dral1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑥 ↔ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) )
19	18	biimpd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑥 → ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) )
20		ax-nul	⊢ ∃ 𝑧 ∀ 𝑦 ¬ 𝑦 ∈ 𝑧
21		elirrv	⊢ ¬ 𝑥 ∈ 𝑥
22	21	ax-gen	⊢ ∀ 𝑥 ¬ 𝑥 ∈ 𝑥
23	22	exgen	⊢ ∃ 𝑥 ∀ 𝑥 ¬ 𝑥 ∈ 𝑥
24	6 7 14 19 20 23	dvelimexcasei	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥