Metamath Proof Explorer

Theorem axpowg2

Description: A generalization of ax-pow in which x and w need not be distinct. This theorem scheme bundles ax-pow with the degenerate instance E. y A. z ( A. x ( x e. z -> x e. x ) -> z e. y ) which is satisfied by the existence of a set that contains all empty sets (see axprlem1 ). 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 axpowg2 
|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  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 ax9v2 
 |-  ( x = v -> ( w e. x -> w e. v ) )
19 18 equcoms 
 |-  ( v = x -> ( w e. x -> w e. v ) )
20 19 imim2d 
 |-  ( v = x -> ( ( w e. z -> w e. x ) -> ( w e. z -> w e. v ) ) )
21 20 al2imi 
 |-  ( A. w v = x -> ( A. w ( w e. z -> w e. x ) -> A. w ( w e. z -> w e. v ) ) )
22 21 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 ) ) )
23 22 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 ) ) )
24 23 eximdv 
 |-  ( 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 ) ) )
25 17 24 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 ) ) ) )
26 axc11r 
 |-  ( A. x x = w -> ( A. w ( w e. z -> w e. x ) -> A. x ( w e. z -> w e. x ) ) )
27 ax8 
 |-  ( x = w -> ( x e. z -> w e. z ) )
28 ax8 
 |-  ( w = x -> ( w e. x -> x e. x ) )
29 28 equcoms 
 |-  ( x = w -> ( w e. x -> x e. x ) )
30 27 29 imim12d 
 |-  ( x = w -> ( ( w e. z -> w e. x ) -> ( x e. z -> x e. x ) ) )
31 30 al2imi 
 |-  ( A. x x = w -> ( A. x ( w e. z -> w e. x ) -> A. x ( x e. z -> x e. x ) ) )
32 26 31 syld 
 |-  ( A. x x = w -> ( A. w ( w e. z -> w e. x ) -> A. x ( x e. z -> x e. x ) ) )
33 32 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 ) ) )
34 33 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 ) ) )
35 34 eximdv 
 |-  ( 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 ) ) )
36 ax-pow 
 |-  E. y A. z ( A. w ( w e. z -> w e. v ) -> z e. y )
37 36 ax-gen 
 |-  A. v E. y A. z ( A. w ( w e. z -> w e. v ) -> z e. y )
38 axprlem1 
 |-  E. y A. z ( A. x -. x e. z -> z e. y )
39 elirrv 
 |-  -. x e. x
40 mtt 
 |-  ( -. x e. x -> ( -. x e. z <-> ( x e. z -> x e. x ) ) )
41 39 40 ax-mp 
 |-  ( -. x e. z <-> ( x e. z -> x e. x ) )
42 41 biimpri 
 |-  ( ( x e. z -> x e. x ) -> -. x e. z )
43 42 alimi 
 |-  ( A. x ( x e. z -> x e. x ) -> A. x -. x e. z )
44 43 imim1i 
 |-  ( ( A. x -. x e. z -> z e. y ) -> ( A. x ( x e. z -> x e. x ) -> z e. y ) )
45 44 alimi 
 |-  ( A. z ( A. x -. x e. z -> z e. y ) -> A. z ( A. x ( x e. z -> x e. x ) -> z e. y ) )
46 38 45 eximii 
 |-  E. y A. z ( A. x ( x e. z -> x e. x ) -> z e. y )
47 46 ax-gen 
 |-  A. x E. y A. z ( A. x ( x e. z -> x e. x ) -> z e. y )
48 14 15 25 35 37 47 dvelimalcasei 
 |-  A. x E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
49 48 spi 
 |-  E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )