Metamath Proof Explorer

Theorem axpowg3

Description: A generalization of ax-pow that combines axpowg and axpowg2 into a single theorem scheme. Unlike ax-pow , this scheme lacks a distinct variable condition for y and w as well as for x and w . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 26-May-2026) (New usage is discouraged.)

Ref Expression
Assertion axpowg3 ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y

Proof

Step Hyp Ref Expression
1 nfnae ⊢ Ⅎ y ¬ ∀ x x = w
2 nfv ⊢ Ⅎ z ¬ ∀ x x = w
3 nfnae ⊢ Ⅎ w ¬ ∀ x x = w
4 nfcvf ⊢ ¬ ∀ x x = w → Ⅎ _ x w
5 nfcvd ⊢ ¬ ∀ x x = w → Ⅎ _ x z
6 4 5 nfeld ⊢ ¬ ∀ x x = w → Ⅎ x w ∈ z
7 nfcvd ⊢ ¬ ∀ x x = w → Ⅎ _ x v
8 4 7 nfeld ⊢ ¬ ∀ x x = w → Ⅎ x w ∈ v
9 6 8 nfimd ⊢ ¬ ∀ x x = w → Ⅎ x w ∈ z → w ∈ v
10 3 9 nfald ⊢ ¬ ∀ x x = w → Ⅎ x ∀ w w ∈ z → w ∈ v
11 nfvd ⊢ ¬ ∀ x x = w → Ⅎ x z ∈ y
12 10 11 nfimd ⊢ ¬ ∀ x x = w → Ⅎ x ∀ w w ∈ z → w ∈ v → z ∈ y
13 2 12 nfald ⊢ ¬ ∀ x x = w → Ⅎ x ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y
14 1 13 nfexd ⊢ ¬ ∀ x x = w → Ⅎ x ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y
15 nfvd ⊢ ¬ ∀ x x = w → Ⅎ v ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
16 dveeq2 ⊢ ¬ ∀ w w = x → v = x → ∀ w v = x
17 16 naecoms ⊢ ¬ ∀ x x = w → v = x → ∀ w v = x
18 nfv ⊢ Ⅎ y v = x
19 18 nfal ⊢ Ⅎ y ∀ w v = x
20 ax9v2 ⊢ x = v → w ∈ x → w ∈ v
21 20 equcoms ⊢ v = x → w ∈ x → w ∈ v
22 21 imim2d ⊢ v = x → w ∈ z → w ∈ x → w ∈ z → w ∈ v
23 22 al2imi ⊢ ∀ w v = x → ∀ w w ∈ z → w ∈ x → ∀ w w ∈ z → w ∈ v
24 23 imim1d ⊢ ∀ w v = x → ∀ w w ∈ z → w ∈ v → z ∈ y → ∀ w w ∈ z → w ∈ x → z ∈ y
25 24 alimdv ⊢ ∀ w v = x → ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y → ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
26 19 25 eximd ⊢ ∀ w v = x → ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y → ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
27 17 26 syl6 ⊢ ¬ ∀ x x = w → v = x → ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y → ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
28 nfae ⊢ Ⅎ y ∀ x x = w
29 axc11r ⊢ ∀ x x = w → ∀ w w ∈ z → w ∈ x → ∀ x w ∈ z → w ∈ x
30 ax8 ⊢ x = w → x ∈ z → w ∈ z
31 ax8 ⊢ w = x → w ∈ x → x ∈ x
32 31 equcoms ⊢ x = w → w ∈ x → x ∈ x
33 30 32 imim12d ⊢ x = w → w ∈ z → w ∈ x → x ∈ z → x ∈ x
34 33 al2imi ⊢ ∀ x x = w → ∀ x w ∈ z → w ∈ x → ∀ x x ∈ z → x ∈ x
35 29 34 syld ⊢ ∀ x x = w → ∀ w w ∈ z → w ∈ x → ∀ x x ∈ z → x ∈ x
36 35 imim1d ⊢ ∀ x x = w → ∀ x x ∈ z → x ∈ x → z ∈ y → ∀ w w ∈ z → w ∈ x → z ∈ y
37 36 alimdv ⊢ ∀ x x = w → ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y → ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
38 28 37 eximd ⊢ ∀ x x = w → ∃ y ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y → ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
39 axpowg ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y
40 39 ax-gen ⊢ ∀ v ∃ y ∀ z ∀ w w ∈ z → w ∈ v → z ∈ y
41 axprlem1 ⊢ ∃ y ∀ z ∀ x ¬ x ∈ z → z ∈ y
42 elirrv ⊢ ¬ x ∈ x
43 mtt ⊢ ¬ x ∈ x → ¬ x ∈ z ↔ x ∈ z → x ∈ x
44 42 43 ax-mp ⊢ ¬ x ∈ z ↔ x ∈ z → x ∈ x
45 44 biimpri ⊢ x ∈ z → x ∈ x → ¬ x ∈ z
46 45 alimi ⊢ ∀ x x ∈ z → x ∈ x → ∀ x ¬ x ∈ z
47 46 imim1i ⊢ ∀ x ¬ x ∈ z → z ∈ y → ∀ x x ∈ z → x ∈ x → z ∈ y
48 47 alimi ⊢ ∀ z ∀ x ¬ x ∈ z → z ∈ y → ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y
49 41 48 eximii ⊢ ∃ y ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y
50 49 ax-gen ⊢ ∀ x ∃ y ∀ z ∀ x x ∈ z → x ∈ x → z ∈ y
51 14 15 27 38 40 50 dvelimalcasei ⊢ ∀ x ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
52 51 spi ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y