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 
|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )

Proof

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