Theorem axpowg3 35336

Description: A generalization of ax-pow 5301 that combines axpowg 35334 and axpowg2 35335 into a single theorem scheme. Unlike ax-pow 5301, this scheme lacks a distinct variable condition for 𝑦 and 𝑤 as well as for 𝑥 and 𝑤. 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
axpowg3	⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

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

Proof of Theorem axpowg3

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfnae 2442	. . . 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		nfv 1921	. . . . . 6 ⊢ Ⅎ𝑦 𝑣 = 𝑥
19	18	nfal 2332	. . . . 5 ⊢ Ⅎ𝑦∀𝑤 𝑣 = 𝑥
20		ax9v2 2132	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
21	20	equcoms 2027	. . . . . . . . 9 ⊢ (𝑣 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
22	21	imim2d 57	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
23	22	al2imi 1822	. . . . . . 7 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
24	23	imim1d 82	. . . . . 6 ⊢ (∀𝑤 𝑣 = 𝑥 → ((∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
25	24	alimdv 1923	. . . . 5 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
26	19, 25	eximd 2228	. . . 4 ⊢ (∀𝑤 𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
27	17, 26	syl6 35	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))))
28		nfae 2441	. . . 4 ⊢ Ⅎ𝑦∀𝑥 𝑥 = 𝑤
29		axc11r 2376	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)))
30		ax8 2125	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑧 → 𝑤 ∈ 𝑧))
31		ax8 2125	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
32	31	equcoms 2027	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
33	30, 32	imim12d 81	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
34	33	al2imi 1822	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
35	29, 34	syld 47	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
36	35	imim1d 82	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
37	36	alimdv 1923	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
38	28, 37	eximd 2228	. . 3 ⊢ (∀𝑥 𝑥 = 𝑤 → (∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
39		axpowg 35334	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
40	39	ax-gen 1802	. . 3 ⊢ ∀𝑣∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
41		axprlem1 5359	. . . . 5 ⊢ ∃𝑦∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦)
42		elirrv 9509	. . . . . . . . . 10 ⊢ ¬ 𝑥 ∈ 𝑥
43		mtt 365	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝑥 → (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
44	42, 43	ax-mp 5	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥))
45	44	biimpri 229	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ¬ 𝑥 ∈ 𝑧)
46	45	alimi 1818	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ∀𝑥 ¬ 𝑥 ∈ 𝑧)
47	46	imim1i 63	. . . . . 6 ⊢ ((∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
48	47	alimi 1818	. . . . 5 ⊢ (∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
49	41, 48	eximii 1844	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
50	49	ax-gen 1802	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
51	14, 15, 27, 38, 40, 50	dvelimalcasei 35265	. 2 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
52	51	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)