Theorem pwex 4630

Description: Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Hypothesis

Ref	Expression
zfpowcl.1	|- A e. _V

Assertion

Ref	Expression
pwex	|- ~P A e. _V

Proof of Theorem pwex

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfpowcl.1	. 2 |- A e. _V
2		pweq 4013	. . 3 |- ( z = A -> ~P z = ~P A )
3	2	eleq1d 2536	. 2 |- ( z = A -> ( ~P z e. _V <-> ~P A e. _V ) )
4		df-pw 4012	. . 3 |- ~P z = { y | y C_ z }
5		axpow2 4627	. . . . . 6 |- E. x A. y ( y C_ z -> y e. x )
6	5	bm1.3ii 4571	. . . . 5 |- E. x A. y ( y e. x <-> y C_ z )
7		abeq2 2591	. . . . . 6 |- ( x = { y | y C_ z } <-> A. y ( y e. x <-> y C_ z ) )
8	7	exbii 1644	. . . . 5 |- ( E. x x = { y | y C_ z } <-> E. x A. y ( y e. x <-> y C_ z ) )
9	6, 8	mpbir 209	. . . 4 |- E. x x = { y | y C_ z }
10	9	issetri 3120	. . 3 |- { y | y C_ z } e. _V
11	4, 10	eqeltri 2551	. 2 |- ~P z e. _V
12	1, 3, 11	vtocl 3165	1 |- ~P A e. _V

Syntax hints:   <-> wb 184   A.wal 1377   = wceq 1379   E.wex 1596   e. wcel 1767   {cab 2452   _Vcvv 3113   C_ wss 3476   ~Pcpw 4010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-pow 4625

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012

This theorem is referenced by:  pwexg  4631  p0ex  4634  pp0ex  4636  ord3ex  4637  abexssex  6766  fnpm  7428  canth2  7670  dffi3  7891  inf3lem7  8051  r1sucg  8187  r1pwOLD  8264  rankuni  8281  rankc2  8289  rankxpu  8294  rankmapu  8296  rankxplim  8297  r0weon  8390  aceq3lem  8501  dfac5lem4  8507  dfac2a  8510  dfac2  8511  dfac8  8515  dfac13  8522  ackbij1lem5  8604  ackbij1lem8  8607  ackbij2lem2  8620  ackbij2lem3  8621  fin23lem17  8718  domtriomlem  8822  dominf  8825  axdc2lem  8828  axdc3lem  8830  numthcor  8874  axdclem2  8900  alephsucpw  8945  dominfac  8948  canthp1lem1  9030  gchac  9059  intwun  9113  wunex2  9116  eltsk2g  9129  inttsk  9152  tskcard  9159  intgru  9192  gruina  9196  axgroth6  9206  npex  9364  axcnex  9524  pnfxr  11321  mnfxr  11323  ixxex  11540  prdsval  14710  prdsds  14719  prdshom  14722  ismre  14845  fnmre  14846  fnmrc  14862  mrcfval  14863  mrisval  14885  mreacs  14913  wunfunc  15126  catcfuccl  15294  catcxpccl  15334  lubfval  15465  glbfval  15478  isacs5lem  15656  issubm  15797  issubg  16006  cntzfval  16163  pmtrfval  16281  sylow1lem2  16425  lsmfval  16464  pj1fval  16518  issubrg  17229  lssset  17380  lspfval  17419  islbs  17522  lbsext  17609  lbsexg  17610  sraval  17622  aspval  17776  ocvfval  18492  cssval  18508  isobs  18546  islinds  18639  istopon  19221  tgdom  19274  fncld  19317  leordtval2  19507  cnpfval  19529  iscnp2  19534  kgenf  19805  xkoopn  19853  xkouni  19863  dfac14  19882  xkoccn  19883  prdstopn  19892  xkoco1cn  19921  xkoco2cn  19922  xkococn  19924  xkoinjcn  19951  isfbas  20093  uzrest  20161  acufl  20181  alexsubALTlem2  20311  tsmsval2  20391  ustfn  20467  ustn0  20486  ishtpy  21235  vitali  21785  sspval  25340  shex  25833  hsupval  25956  fpwrelmap  27256  fpwrelmapffs  27257  isrnsigaOLD  27780  dmvlsiga  27797  eulerpartlem1  27974  eulerpartgbij  27979  eulerpartlemmf  27982  coinflippv  28090  ballotlemoex  28092  kur14lem9  28326  heibor1lem  29936  heibor  29948  idlval  30041  mzpclval  30289  eldiophb  30322  rpnnen3  30606  dfac11  30640  rgspnval  30750  usgsizedg  31890  usgsizedgALT  31891  usgsizedgALT2  31892  lincop  32108  bj-snglex  33630  psubspset  34558  paddfval  34611  pclfvalN  34703  polfvalN  34718  psubclsetN  34750  docafvalN  35937  djafvalN  35949  dicval  35991  dochfval  36165  djhfval  36212  islpolN  36298