Theorem pwex 4463

Description: Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-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 3851	. . 3 |- ( z = A -> ~P z = ~P A )
3	2	eleq1d 2499	. 2 |- ( z = A -> ( ~P z e. _V <-> ~P A e. _V ) )
4		df-pw 3850	. . 3 |- ~P z = { y | y C_ z }
5		axpow2 4460	. . . . . 6 |- E. x A. y ( y C_ z -> y e. x )
6	5	bm1.3ii 4404	. . . . 5 |- E. x A. y ( y e. x <-> y C_ z )
7		abeq2 2538	. . . . . 6 |- ( x = { y | y C_ z } <-> A. y ( y e. x <-> y C_ z ) )
8	7	exbii 1634	. . . . 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 2969	. . 3 |- { y | y C_ z } e. _V
11	4, 10	eqeltri 2503	. 2 |- ~P z e. _V
12	1, 3, 11	vtocl 3013	1 |- ~P A e. _V

Syntax hints:   <-> wb 184   A.wal 1360   = wceq 1362   E.wex 1589   e. wcel 1755   {cab 2419   _Vcvv 2962   C_ wss 3316   ~Pcpw 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-pow 4458

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850

This theorem is referenced by:  pwexg  4464  p0ex  4467  pp0ex  4469  ord3ex  4470  abexssex  6548  fnpm  7210  canth2  7452  dffi3  7669  inf3lem7  7828  r1sucg  7964  r1pwOLD  8041  rankuni  8058  rankc2  8066  rankxpu  8071  rankmapu  8073  rankxplim  8074  r0weon  8167  aceq3lem  8278  dfac5lem4  8284  dfac2a  8287  dfac2  8288  dfac8  8292  dfac13  8299  ackbij1lem5  8381  ackbij1lem8  8384  ackbij2lem2  8397  ackbij2lem3  8398  fin23lem17  8495  domtriomlem  8599  dominf  8602  axdc2lem  8605  axdc3lem  8607  numthcor  8651  axdclem2  8677  alephsucpw  8722  dominfac  8725  canthp1lem1  8806  gchac  8835  intwun  8889  wunex2  8892  eltsk2g  8905  inttsk  8928  tskcard  8935  intgru  8968  gruina  8972  axgroth6  8982  npex  9142  axcnex  9301  pnfxr  11079  mnfxr  11081  ixxex  11298  prdsval  14375  prdsds  14384  prdshom  14387  ismre  14510  fnmre  14511  fnmrc  14527  mrcfval  14528  mrisval  14550  mreacs  14578  wunfunc  14791  catcfuccl  14959  catcxpccl  14999  lubfval  15130  glbfval  15143  isacs5lem  15321  issubm  15456  issubg  15660  cntzfval  15817  pmtrfval  15935  sylow1lem2  16077  lsmfval  16116  pj1fval  16170  issubrg  16788  lssset  16936  lspfval  16975  islbs  17078  lbsext  17165  lbsexg  17166  sraval  17178  aspval  17320  ocvfval  17932  cssval  17948  isobs  17986  islinds  18079  istopon  18371  tgdom  18424  fncld  18467  leordtval2  18657  cnpfval  18679  iscnp2  18684  kgenf  18955  xkoopn  19003  xkouni  19013  dfac14  19032  xkoccn  19033  prdstopn  19042  xkoco1cn  19071  xkoco2cn  19072  xkococn  19074  xkoinjcn  19101  isfbas  19243  uzrest  19311  acufl  19331  alexsubALTlem2  19461  tsmsval2  19541  ustfn  19617  ustn0  19636  ishtpy  20385  vitali  20934  sspval  23943  shex  24436  hsupval  24559  fpwrelmap  25857  fpwrelmapffs  25858  isrnsigaOLD  26408  dmvlsiga  26425  eulerpartlem1  26597  eulerpartgbij  26602  eulerpartlemmf  26605  coinflippv  26713  ballotlemoex  26715  kur14lem9  26949  heibor1lem  28549  heibor  28561  idlval  28654  mzpclval  28903  eldiophb  28937  rpnnen3  29223  dfac11  29257  rgspnval  29367  lincop  30648  bj-snglex  32046  psubspset  32958  paddfval  33011  pclfvalN  33103  polfvalN  33118  psubclsetN  33150  docafvalN  34337  djafvalN  34349  dicval  34391  dochfval  34565  djhfval  34612  islpolN  34698