Theorem axpowg3 35456

Description: A generalization of ax-pow 5327 that combines axpowg 35454 and axpowg2 35455 into a single theorem scheme. Unlike ax-pow 5327, 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 2406. (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 2468	. . . 4 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑤
2		nfv 1937	. . . . 5 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑤
3		nfnae 2468	. . . . . . 7 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑤
4		nfcvf 2953	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑤)
5		nfcvd 2928	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑧)
6	4, 5	nfeld 2938	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑤 ∈ 𝑧)
7		nfcvd 2928	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑣)
8	4, 7	nfeld 2938	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑤 ∈ 𝑣)
9	6, 8	nfimd 1917	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣))
10	3, 9	nfald 2363	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣))
11		nfvd 1938	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥 𝑧 ∈ 𝑦)
12	10, 11	nfimd 1917	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
13	2, 12	nfald 2363	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
14	1, 13	nfexd 2364	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦))
15		nfvd 1938	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑣∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
16		dveeq2 2412	. . . . 5 ⊢ (¬ ∀𝑤 𝑤 = 𝑥 → (𝑣 = 𝑥 → ∀𝑤 𝑣 = 𝑥))
17	16	naecoms 2463	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑣 = 𝑥 → ∀𝑤 𝑣 = 𝑥))
18		nfv 1937	. . . . . 6 ⊢ Ⅎ𝑦 𝑣 = 𝑥
19	18	nfal 2358	. . . . 5 ⊢ Ⅎ𝑦∀𝑤 𝑣 = 𝑥
20		ax9v2 2158	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
21	20	equcoms 2043	. . . . . . . . 9 ⊢ (𝑣 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑣))
22	21	imim2d 58	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
23	22	al2imi 1838	. . . . . . 7 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣)))
24	23	imim1d 83	. . . . . 6 ⊢ (∀𝑤 𝑣 = 𝑥 → ((∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
25	24	alimdv 1939	. . . . 5 ⊢ (∀𝑤 𝑣 = 𝑥 → (∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
26	19, 25	eximd 2254	. . . 4 ⊢ (∀𝑤 𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
27	17, 26	syl6 36	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑣 = 𝑥 → (∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))))
28		nfae 2467	. . . 4 ⊢ Ⅎ𝑦∀𝑥 𝑥 = 𝑤
29		axc11r 2402	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)))
30		ax8 2151	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑧 → 𝑤 ∈ 𝑧))
31		ax8 2151	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
32	31	equcoms 2043	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑤 ∈ 𝑥 → 𝑥 ∈ 𝑥))
33	30, 32	imim12d 82	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
34	33	al2imi 1838	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
35	29, 34	syld 48	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
36	35	imim1d 83	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → (∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
37	36	alimdv 1939	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
38	28, 37	eximd 2254	. . 3 ⊢ (∀𝑥 𝑥 = 𝑤 → (∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)))
39		axpowg 35454	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
40	39	ax-gen 1818	. . 3 ⊢ ∀𝑣∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑣) → 𝑧 ∈ 𝑦)
41		axprlem1 5385	. . . . 5 ⊢ ∃𝑦∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦)
42		elirrv 9547	. . . . . . . . . 10 ⊢ ¬ 𝑥 ∈ 𝑥
43		mtt 367	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝑥 → (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥)))
44	42, 43	ax-mp 5	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝑧 ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥))
45	44	biimpri 231	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ¬ 𝑥 ∈ 𝑧)
46	45	alimi 1834	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → ∀𝑥 ¬ 𝑥 ∈ 𝑧)
47	46	imim1i 64	. . . . . 6 ⊢ ((∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → (∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
48	47	alimi 1834	. . . . 5 ⊢ (∀𝑧(∀𝑥 ¬ 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝑦) → ∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦))
49	41, 48	eximii 1860	. . . 4 ⊢ ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
50	49	ax-gen 1818	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦)
51	14, 15, 27, 38, 40, 50	dvelimalcasei 35381	. 2 ⊢ ∀𝑥∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
52	51	spi 2222	1 ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀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-pow 5327  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)