Metamath Proof Explorer

Theorem zfcndpow

Description: Axiom of Power Sets ax-pow , reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness" dtru . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Aug-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion zfcndpow 
|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )

Proof

Step Hyp Ref Expression
1 dtru 
 |-  -. A. y y = z
2 exnal 
 |-  ( E. y -. y = z <-> -. A. y y = z )
3 1 2 mpbir 
 |-  E. y -. y = z
4 nfe1 
 |-  F/ y E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y )
5 axpownd 
 |-  ( -. y = z -> E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) )
6 4 5 exlimi 
 |-  ( E. y -. y = z -> E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) )
7 3 6 ax-mp 
 |-  E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y )
8 19.9v 
 |-  ( E. x y e. z <-> y e. z )
9 19.3v 
 |-  ( A. z y e. x <-> y e. x )
10 8 9 imbi12i 
 |-  ( ( E. x y e. z -> A. z y e. x ) <-> ( y e. z -> y e. x ) )
11 10 albii 
 |-  ( A. y ( E. x y e. z -> A. z y e. x ) <-> A. y ( y e. z -> y e. x ) )
12 11 imbi1i 
 |-  ( ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) <-> ( A. y ( y e. z -> y e. x ) -> z e. y ) )
13 12 albii 
 |-  ( A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) <-> A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) )
14 13 exbii 
 |-  ( E. y A. z ( A. y ( E. x y e. z -> A. z y e. x ) -> z e. y ) <-> E. y A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) )
15 7 14 mpbi 
 |-  E. y A. z ( A. y ( y e. z -> y e. x ) -> z e. y )
16 elequ1 
 |-  ( w = y -> ( w e. z <-> y e. z ) )
17 elequ1 
 |-  ( w = y -> ( w e. x <-> y e. x ) )
18 16 17 imbi12d 
 |-  ( w = y -> ( ( w e. z -> w e. x ) <-> ( y e. z -> y e. x ) ) )
19 18 cbvalvw 
 |-  ( A. w ( w e. z -> w e. x ) <-> A. y ( y e. z -> y e. x ) )
20 19 imbi1i 
 |-  ( ( A. w ( w e. z -> w e. x ) -> z e. y ) <-> ( A. y ( y e. z -> y e. x ) -> z e. y ) )
21 20 albii 
 |-  ( A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) <-> A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) )
22 21 exbii 
 |-  ( E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) <-> E. y A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) )
23 15 22 mpbir 
 |-  E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )