Theorem axpowg2 35335

Description: A generalization of ax-pow 5301 in which 𝑥 and 𝑤 need not be distinct. This theorem scheme bundles ax-pow 5301 with the degenerate instance ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) which is satisfied by the existence of a set that contains all empty sets (see axprlem1 5359). Usage of this theorem is discouraged because it depends on ax-13 2380. (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 1921	. . . 4 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑤
2		nfv 1921	. . . . 5 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑤
3		nfnae 2442	. . . . . . 7 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑤
4		nfcvf 2928	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑤)
5		nfcvd 2903	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑧)
6	4, 5	nfeld 2913	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑤 ∈ 𝑧)
7		nfcvd 2903	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑣)
8	4, 7	nfeld 2913	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑤 ∈ 𝑣)
9	6, 8	nfimd 1901	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣))
10	3, 9	nfald 2337	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣))
11		nfvd 1922	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑧 ∈ 𝑦)
12	10, 11	nfimd 1901	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
13	2, 12	nfald 2337	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
14	1, 13	nfexd 2338	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
15		nfvd 1922	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑣∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
16		dveeq2 2386	. . . . 5 ⊢ (¬ ∀𝑤 𝑤 = 𝑥 → (𝑣 = 𝑥 → ∀𝑤 𝑣 = 𝑥))
17	16	naecoms 2437	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑣 = 𝑥 → ∀𝑤 𝑣 = 𝑥))
18		ax9v2 2132	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
19	18	equcoms 2027	. . . . . . . . 9 ⊢ (𝑣 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
20	19	imim2d 57	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
21	20	al2imi 1822	. . . . . . 7 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
22	21	imim1d 82	. . . . . 6 ⊢ (∀𝑤 𝑣 = 𝑥 → ((∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
23	22	alimdv 1923	. . . . 5 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
24	23	eximdv 1924	. . . 4 ⊢ (∀𝑤 𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
25	17, 24	syl6 35	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))))
26		axc11r 2376	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)))
27		ax8 2125	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑧 → 𝑤 ∈ 𝑧))
28		ax8 2125	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
29	28	equcoms 2027	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
30	27, 29	imim12d 81	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
31	30	al2imi 1822	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
32	26, 31	syld 47	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
33	32	imim1d 82	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
34	33	alimdv 1923	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
35	34	eximdv 1924	. . 3 ⊢ (∀𝑥 𝑥 = 𝑤 → (∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
36		ax-pow 5301	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
37	36	ax-gen 1802	. . 3 ⊢ ∀𝑣∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
38		axprlem1 5359	. . . . 5 ⊢ ∃𝑦∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦)
39		elirrv 9509	. . . . . . . . . 10 ⊢ ¬ 𝑥 ∈ 𝑥
40		mtt 365	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝑥 → (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
41	39, 40	ax-mp 5	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥))
42	41	biimpri 229	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ¬ 𝑥 ∈ 𝑧)
43	42	alimi 1818	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ∀𝑥 ¬ 𝑥 ∈ 𝑧)
44	43	imim1i 63	. . . . . 6 ⊢ ((∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
45	44	alimi 1818	. . . . 5 ⊢ (∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
46	38, 45	eximii 1844	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
47	46	ax-gen 1802	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
48	14, 15, 25, 35, 37, 47	dvelimalcasei 35265	. 2 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
49	48	spi 2196	1 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-13 2380  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-reg 9504

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-cleq 2732  df-clel 2815  df-nfc 2889

This theorem is referenced by: (None)