Theorem axpowg2 35407

Description: A generalization of ax-pow 5321 in which 𝑥 and 𝑤 need not be distinct. This theorem scheme bundles ax-pow 5321 with the degenerate instance ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) which is satisfied by the existence of a set that contains all empty sets (see axprlem1 5379). Usage of this theorem is discouraged because it depends on ax-13 2402. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)

Assertion

Ref	Expression
axpowg2	⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

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

Proof of Theorem axpowg2

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1933	. . . 4 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑤
2		nfv 1933	. . . . 5 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑤
3		nfnae 2464	. . . . . . 7 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑤
4		nfcvf 2949	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑤)
5		nfcvd 2924	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑧)
6	4, 5	nfeld 2934	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑤 ∈ 𝑧)
7		nfcvd 2924	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑣)
8	4, 7	nfeld 2934	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑤 ∈ 𝑣)
9	6, 8	nfimd 1913	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣))
10	3, 9	nfald 2359	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣))
11		nfvd 1934	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑧 ∈ 𝑦)
12	10, 11	nfimd 1913	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
13	2, 12	nfald 2359	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
14	1, 13	nfexd 2360	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
15		nfvd 1934	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑣∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
16		dveeq2 2408	. . . . 5 ⊢ (¬ ∀𝑤 𝑤 = 𝑥 → (𝑣 = 𝑥 → ∀𝑤 𝑣 = 𝑥))
17	16	naecoms 2459	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑣 = 𝑥 → ∀𝑤 𝑣 = 𝑥))
18		ax9v2 2154	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
19	18	equcoms 2039	. . . . . . . . 9 ⊢ (𝑣 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
20	19	imim2d 57	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
21	20	al2imi 1834	. . . . . . 7 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
22	21	imim1d 82	. . . . . 6 ⊢ (∀𝑤 𝑣 = 𝑥 → ((∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
23	22	alimdv 1935	. . . . 5 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
24	23	eximdv 1936	. . . 4 ⊢ (∀𝑤 𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
25	17, 24	syl6 35	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))))
26		axc11r 2398	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)))
27		ax8 2147	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑧 → 𝑤 ∈ 𝑧))
28		ax8 2147	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
29	28	equcoms 2039	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
30	27, 29	imim12d 81	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
31	30	al2imi 1834	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
32	26, 31	syld 47	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
33	32	imim1d 82	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
34	33	alimdv 1935	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
35	34	eximdv 1936	. . 3 ⊢ (∀𝑥 𝑥 = 𝑤 → (∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
36		ax-pow 5321	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
37	36	ax-gen 1814	. . 3 ⊢ ∀𝑣∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
38		axprlem1 5379	. . . . 5 ⊢ ∃𝑦∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦)
39		elirrv 9542	. . . . . . . . . 10 ⊢ ¬ 𝑥 ∈ 𝑥
40		mtt 366	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝑥 → (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
41	39, 40	ax-mp 5	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥))
42	41	biimpri 230	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ¬ 𝑥 ∈ 𝑧)
43	42	alimi 1830	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ∀𝑥 ¬ 𝑥 ∈ 𝑧)
44	43	imim1i 63	. . . . . 6 ⊢ ((∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
45	44	alimi 1830	. . . . 5 ⊢ (∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
46	38, 45	eximii 1856	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
47	46	ax-gen 1814	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
48	14, 15, 25, 35, 37, 47	dvelimalcasei 35335	. 2 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
49	48	spi 2218	1 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-13 2402  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-reg 9537

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-cleq 2753  df-clel 2836  df-nfc 2910

This theorem is referenced by: (None)