Theorem axsepg2 35448

Description: A generalization of ax-sep 5251 in which 𝑥 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5251 with the degenerate instance ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)) which is satisfied by the existence of the empty set. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by BTernaryTau, 21-May-2026.) (New usage is discouraged.)

Assertion

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

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦,𝑧

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem axsepg2

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1937	. . . 4 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑥
2		nfnae 2468	. . . . 5 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑥
3		nfcvf 2953	. . . . . . 7 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧𝑥)
4		nfcvd 2928	. . . . . . 7 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧𝑦)
5	3, 4	nfeld 2938	. . . . . 6 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧 𝑥 ∈ 𝑦)
6		nfcvd 2928	. . . . . . . 8 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧𝑤)
7	3, 6	nfeld 2938	. . . . . . 7 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧 𝑥 ∈ 𝑤)
8		nfvd 1938	. . . . . . 7 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧𝜑)
9	7, 8	nfand 1920	. . . . . 6 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧(𝑥 ∈ 𝑤 ∧ 𝜑))
10	5, 9	nfbid 1925	. . . . 5 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)))
11	2, 10	nfald 2363	. . . 4 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)))
12	1, 11	nfexd 2364	. . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)))
13		nfvd 1938	. . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑤∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
14		dveeq2 2412	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑤 = 𝑧 → ∀𝑥 𝑤 = 𝑧))
15	14	naecoms 2463	. . . 4 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (𝑤 = 𝑧 → ∀𝑥 𝑤 = 𝑧))
16		elequ2 2160	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑧))
17	16	anbi1d 642	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → ((𝑥 ∈ 𝑤 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
18	17	bibi2d 345	. . . . . . 7 ⊢ (𝑤 = 𝑧 → ((𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
19	18	biimpd 232	. . . . . 6 ⊢ (𝑤 = 𝑧 → ((𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)) → (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
20	19	al2imi 1838	. . . . 5 ⊢ (∀𝑥 𝑤 = 𝑧 → (∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
21	20	eximdv 1940	. . . 4 ⊢ (∀𝑥 𝑤 = 𝑧 → (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
22	15, 21	syl6 36	. . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (𝑤 = 𝑧 → (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))))
23		elequ1 2152	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
24		elequ1 2152	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
25	24	anbi1d 642	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
26	23, 25	bibi12d 348	. . . . . . 7 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
27	26	biimpd 232	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)) → (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
28	27	al2imi 1838	. . . . 5 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)) → ∀𝑧(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
29		axc11 2464	. . . . 5 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑧(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
30	28, 29	syld 48	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
31	30	eximdv 1940	. . 3 ⊢ (∀𝑧 𝑧 = 𝑥 → (∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))
32		ax-sep 5251	. . . 4 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑))
33	32	ax-gen 1818	. . 3 ⊢ ∀𝑤∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑤 ∧ 𝜑))
34		ax-nul 5261	. . . . 5 ⊢ ∃𝑦∀𝑧 ¬ 𝑧 ∈ 𝑦
35		elirrv 9547	. . . . . . . . 9 ⊢ ¬ 𝑧 ∈ 𝑧
36	35	intnanr 492	. . . . . . . 8 ⊢ ¬ (𝑧 ∈ 𝑧 ∧ 𝜑)
37	36	nbn 375	. . . . . . 7 ⊢ (¬ 𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)))
38	37	biimpi 219	. . . . . 6 ⊢ (¬ 𝑧 ∈ 𝑦 → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)))
39	38	alimi 1834	. . . . 5 ⊢ (∀𝑧 ¬ 𝑧 ∈ 𝑦 → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)))
40	34, 39	eximii 1860	. . . 4 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑))
41	40	ax-gen 1818	. . 3 ⊢ ∀𝑧∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑))
42	12, 13, 22, 31, 33, 41	dvelimalcasei 35381	. 2 ⊢ ∀𝑧∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
43	42	spi 2222	1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-13 2406  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-reg 9542

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807  df-cleq 2757  df-clel 2840  df-nfc 2914

This theorem is referenced by: (None)