Theorem pwex 4582

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 3970	. . 3 |- ( z = A -> ~P z = ~P A )
3	2	eleq1d 2523	. 2 |- ( z = A -> ( ~P z e. _V <-> ~P A e. _V ) )
4		df-pw 3969	. . 3 |- ~P z = { y | y C_ z }
5		axpow2 4579	. . . . . 6 |- E. x A. y ( y C_ z -> y e. x )
6	5	bm1.3ii 4523	. . . . 5 |- E. x A. y ( y e. x <-> y C_ z )
7		abeq2 2578	. . . . . 6 |- ( x = { y | y C_ z } <-> A. y ( y e. x <-> y C_ z ) )
8	7	exbii 1635	. . . . 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 3083	. . 3 |- { y | y C_ z } e. _V
11	4, 10	eqeltri 2538	. 2 |- ~P z e. _V
12	1, 3, 11	vtocl 3128	1 |- ~P A e. _V

Syntax hints:   <-> wb 184   A.wal 1368   = wceq 1370   E.wex 1587   e. wcel 1758   {cab 2439   _Vcvv 3076   C_ wss 3435   ~Pcpw 3967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-pow 4577

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3078  df-in 3442  df-ss 3449  df-pw 3969

This theorem is referenced by:  pwexg  4583  p0ex  4586  pp0ex  4588  ord3ex  4589  abexssex  6668  fnpm  7331  canth2  7573  dffi3  7791  inf3lem7  7950  r1sucg  8086  r1pwOLD  8163  rankuni  8180  rankc2  8188  rankxpu  8193  rankmapu  8195  rankxplim  8196  r0weon  8289  aceq3lem  8400  dfac5lem4  8406  dfac2a  8409  dfac2  8410  dfac8  8414  dfac13  8421  ackbij1lem5  8503  ackbij1lem8  8506  ackbij2lem2  8519  ackbij2lem3  8520  fin23lem17  8617  domtriomlem  8721  dominf  8724  axdc2lem  8727  axdc3lem  8729  numthcor  8773  axdclem2  8799  alephsucpw  8844  dominfac  8847  canthp1lem1  8929  gchac  8958  intwun  9012  wunex2  9015  eltsk2g  9028  inttsk  9051  tskcard  9058  intgru  9091  gruina  9095  axgroth6  9105  npex  9265  axcnex  9424  pnfxr  11202  mnfxr  11204  ixxex  11421  prdsval  14511  prdsds  14520  prdshom  14523  ismre  14646  fnmre  14647  fnmrc  14663  mrcfval  14664  mrisval  14686  mreacs  14714  wunfunc  14927  catcfuccl  15095  catcxpccl  15135  lubfval  15266  glbfval  15279  isacs5lem  15457  issubm  15593  issubg  15799  cntzfval  15956  pmtrfval  16074  sylow1lem2  16218  lsmfval  16257  pj1fval  16311  issubrg  16987  lssset  17137  lspfval  17176  islbs  17279  lbsext  17366  lbsexg  17367  sraval  17379  aspval  17521  ocvfval  18215  cssval  18231  isobs  18269  islinds  18362  istopon  18661  tgdom  18714  fncld  18757  leordtval2  18947  cnpfval  18969  iscnp2  18974  kgenf  19245  xkoopn  19293  xkouni  19303  dfac14  19322  xkoccn  19323  prdstopn  19332  xkoco1cn  19361  xkoco2cn  19362  xkococn  19364  xkoinjcn  19391  isfbas  19533  uzrest  19601  acufl  19621  alexsubALTlem2  19751  tsmsval2  19831  ustfn  19907  ustn0  19926  ishtpy  20675  vitali  21225  sspval  24272  shex  24765  hsupval  24888  fpwrelmap  26183  fpwrelmapffs  26184  isrnsigaOLD  26699  dmvlsiga  26716  eulerpartlem1  26893  eulerpartgbij  26898  eulerpartlemmf  26901  coinflippv  27009  ballotlemoex  27011  kur14lem9  27245  heibor1lem  28855  heibor  28867  idlval  28960  mzpclval  29208  eldiophb  29242  rpnnen3  29528  dfac11  29562  rgspnval  29672  lincop  31060  bj-snglex  32783  psubspset  33711  paddfval  33764  pclfvalN  33856  polfvalN  33871  psubclsetN  33903  docafvalN  35090  djafvalN  35102  dicval  35144  dochfval  35318  djhfval  35365  islpolN  35451