Theorem axsepg2

Description: A generalization of ax-sep in which x and z need not be distinct. This theorem scheme bundles ax-sep with the degenerate instance E. y A. z ( z e. y <-> ( z e. z /\ ph ) ) which is satisfied by the existence of the empty set. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 21-May-2026) (New usage is discouraged.)

	Ref	Expression
Assertion	axsepg2	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑦 ¬ ∀ 𝑧 𝑧 = 𝑥
2		nfnae	⊢ Ⅎ 𝑥 ¬ ∀ 𝑧 𝑧 = 𝑥
3		nfcvf	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑥 )
4		nfcvd	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑦 )
5	3 4	nfeld	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑥 ∈ 𝑦 )
6		nfcvd	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑤 )
7	3 6	nfeld	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑥 ∈ 𝑤 )
8		nfvd	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝜑 )
9	7 8	nfand	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
10	5 9	nfbid	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
11	2 10	nfald	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
12	1 11	nfexd	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
13		nfvd	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑤 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
14		dveeq2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( 𝑤 = 𝑧 → ∀ 𝑥 𝑤 = 𝑧 ) )
15	14	naecoms	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( 𝑤 = 𝑧 → ∀ 𝑥 𝑤 = 𝑧 ) )
16		elequ2	⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑧 ) )
17	16	anbi1d	⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
18	17	bibi2d	⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
19	18	biimpd	⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
20	19	al2imi	⊢ ( ∀ 𝑥 𝑤 = 𝑧 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
21	20	eximdv	⊢ ( ∀ 𝑥 𝑤 = 𝑧 → ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
22	15 21	syl6	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( 𝑤 = 𝑧 → ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) ) )
23		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
24		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
25	24	anbi1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
26	23 25	bibi12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
27	26	biimpd	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
28	27	al2imi	⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑧 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
29		axc11	⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
30	28 29	syld	⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
31	30	eximdv	⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
32		ax-sep	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
33	32	ax-gen	⊢ ∀ 𝑤 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
34		ax-nul	⊢ ∃ 𝑦 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦
35		elirrv	⊢ ¬ 𝑧 ∈ 𝑧
36	35	intnanr	⊢ ¬ ( 𝑧 ∈ 𝑧 ∧ 𝜑 )
37	36	nbn	⊢ ( ¬ 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) )
38	37	biimpi	⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) )
39	38	alimi	⊢ ( ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) )
40	34 39	eximii	⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) )
41	40	ax-gen	⊢ ∀ 𝑧 ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) )
42	12 13 22 31 33 41	dvelimalcasei	⊢ ∀ 𝑧 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
43	42	spi	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )