Theorem pwex 4548

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 3930	. . 3 |- ( z = A -> ~P z = ~P A )
3	2	eleq1d 2451	. 2 |- ( z = A -> ( ~P z e. _V <-> ~P A e. _V ) )
4		df-pw 3929	. . 3 |- ~P z = { y | y C_ z }
5		axpow2 4545	. . . . . 6 |- E. x A. y ( y C_ z -> y e. x )
6	5	bm1.3ii 4491	. . . . 5 |- E. x A. y ( y e. x <-> y C_ z )
7		abeq2 2506	. . . . . 6 |- ( x = { y | y C_ z } <-> A. y ( y e. x <-> y C_ z ) )
8	7	exbii 1675	. . . . 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 3041	. . 3 |- { y | y C_ z } e. _V
11	4, 10	eqeltri 2466	. 2 |- ~P z e. _V
12	1, 3, 11	vtocl 3086	1 |- ~P A e. _V

Syntax hints:   <-> wb 184   A.wal 1397   = wceq 1399   E.wex 1620   e. wcel 1826   {cab 2367   _Vcvv 3034   C_ wss 3389   ~Pcpw 3927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-pow 4543

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-v 3036  df-in 3396  df-ss 3403  df-pw 3929

This theorem is referenced by:  pwexg  4549  p0ex  4552  pp0ex  4554  ord3ex  4555  abexssex  6681  fnpm  7346  canth2  7589  dffi3  7806  inf3lem7  7965  r1sucg  8100  r1pwALT  8177  rankuni  8194  rankc2  8202  rankxpu  8207  rankmapu  8209  rankxplim  8210  r0weon  8303  aceq3lem  8414  dfac5lem4  8420  dfac2a  8423  dfac2  8424  dfac8  8428  dfac13  8435  ackbij1lem5  8517  ackbij1lem8  8520  ackbij2lem2  8533  ackbij2lem3  8534  fin23lem17  8631  domtriomlem  8735  dominf  8738  axdc2lem  8741  axdc3lem  8743  numthcor  8787  axdclem2  8813  alephsucpw  8858  dominfac  8861  canthp1lem1  8941  gchac  8970  intwun  9024  wunex2  9027  eltsk2g  9040  inttsk  9063  tskcard  9070  intgru  9103  gruina  9107  axgroth6  9117  npex  9275  axcnex  9435  pnfxr  11242  mnfxr  11244  ixxex  11461  prdsval  14862  prdsds  14871  prdshom  14874  ismre  14997  fnmre  14998  fnmrc  15014  mrcfval  15015  mrisval  15037  mreacs  15065  wunfunc  15305  catcfuccl  15505  catcxpccl  15593  lubfval  15725  glbfval  15738  isacs5lem  15916  issubm  16095  issubg  16318  cntzfval  16475  pmtrfval  16592  sylow1lem2  16736  lsmfval  16775  pj1fval  16829  issubrg  17542  lssset  17693  lspfval  17732  islbs  17835  lbsext  17922  lbsexg  17923  sraval  17935  aspval  18090  ocvfval  18788  cssval  18804  isobs  18842  islinds  18929  istopon  19511  tgdom  19565  fncld  19608  leordtval2  19799  cnpfval  19821  iscnp2  19826  kgenf  20127  xkoopn  20175  xkouni  20185  dfac14  20204  xkoccn  20205  prdstopn  20214  xkoco1cn  20243  xkoco2cn  20244  xkococn  20246  xkoinjcn  20273  isfbas  20415  uzrest  20483  acufl  20503  alexsubALTlem2  20633  tsmsval2  20713  ustfn  20789  ustn0  20808  ishtpy  21557  vitali  22107  sspval  25753  shex  26246  hsupval  26369  fpwrelmap  27706  fpwrelmapffs  27707  isrnsigaOLD  28261  dmvlsiga  28278  eulerpartlem1  28489  eulerpartgbij  28494  eulerpartlemmf  28497  coinflippv  28605  ballotlemoex  28607  kur14lem9  28847  mpstval  29084  mclsrcl  29110  mclsval  29112  heibor1lem  30471  heibor  30483  idlval  30576  mzpclval  30823  eldiophb  30855  rpnnen3  31140  dfac11  31174  rgspnval  31285  usgsizedg  32713  usgsizedgALT  32714  usgsizedgALT2  32715  issubmgm  32795  lincop  33209  bj-snglex  34879  psubspset  35881  paddfval  35934  pclfvalN  36026  polfvalN  36041  psubclsetN  36073  docafvalN  37262  djafvalN  37274  dicval  37316  dochfval  37490  djhfval  37537  islpolN  37623  pwinfi  38178