Theorem pwex 4470

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 3858	. . 3 |- ( z = A -> ~P z = ~P A )
3	2	eleq1d 2504	. 2 |- ( z = A -> ( ~P z e. _V <-> ~P A e. _V ) )
4		df-pw 3857	. . 3 |- ~P z = { y | y C_ z }
5		axpow2 4467	. . . . . 6 |- E. x A. y ( y C_ z -> y e. x )
6	5	bm1.3ii 4411	. . . . 5 |- E. x A. y ( y e. x <-> y C_ z )
7		abeq2 2543	. . . . . 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 2974	. . 3 |- { y | y C_ z } e. _V
11	4, 10	eqeltri 2508	. 2 |- ~P z e. _V
12	1, 3, 11	vtocl 3019	1 |- ~P A e. _V

Syntax hints:   <-> wb 184   A.wal 1367   = wceq 1369   E.wex 1586   e. wcel 1756   {cab 2424   _Vcvv 2967   C_ wss 3323   ~Pcpw 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-pow 4465

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2969  df-in 3330  df-ss 3337  df-pw 3857

This theorem is referenced by:  pwexg  4471  p0ex  4474  pp0ex  4476  ord3ex  4477  abexssex  6554  fnpm  7214  canth2  7456  dffi3  7673  inf3lem7  7832  r1sucg  7968  r1pwOLD  8045  rankuni  8062  rankc2  8070  rankxpu  8075  rankmapu  8077  rankxplim  8078  r0weon  8171  aceq3lem  8282  dfac5lem4  8288  dfac2a  8291  dfac2  8292  dfac8  8296  dfac13  8303  ackbij1lem5  8385  ackbij1lem8  8388  ackbij2lem2  8401  ackbij2lem3  8402  fin23lem17  8499  domtriomlem  8603  dominf  8606  axdc2lem  8609  axdc3lem  8611  numthcor  8655  axdclem2  8681  alephsucpw  8726  dominfac  8729  canthp1lem1  8811  gchac  8840  intwun  8894  wunex2  8897  eltsk2g  8910  inttsk  8933  tskcard  8940  intgru  8973  gruina  8977  axgroth6  8987  npex  9147  axcnex  9306  pnfxr  11084  mnfxr  11086  ixxex  11303  prdsval  14385  prdsds  14394  prdshom  14397  ismre  14520  fnmre  14521  fnmrc  14537  mrcfval  14538  mrisval  14560  mreacs  14588  wunfunc  14801  catcfuccl  14969  catcxpccl  15009  lubfval  15140  glbfval  15153  isacs5lem  15331  issubm  15466  issubg  15672  cntzfval  15829  pmtrfval  15947  sylow1lem2  16089  lsmfval  16128  pj1fval  16182  issubrg  16845  lssset  16995  lspfval  17034  islbs  17137  lbsext  17224  lbsexg  17225  sraval  17237  aspval  17379  ocvfval  18071  cssval  18087  isobs  18125  islinds  18218  istopon  18510  tgdom  18563  fncld  18606  leordtval2  18796  cnpfval  18818  iscnp2  18823  kgenf  19094  xkoopn  19142  xkouni  19152  dfac14  19171  xkoccn  19172  prdstopn  19181  xkoco1cn  19210  xkoco2cn  19211  xkococn  19213  xkoinjcn  19240  isfbas  19382  uzrest  19450  acufl  19470  alexsubALTlem2  19600  tsmsval2  19680  ustfn  19756  ustn0  19775  ishtpy  20524  vitali  21073  sspval  24089  shex  24582  hsupval  24705  fpwrelmap  26001  fpwrelmapffs  26002  isrnsigaOLD  26524  dmvlsiga  26541  eulerpartlem1  26719  eulerpartgbij  26724  eulerpartlemmf  26727  coinflippv  26835  ballotlemoex  26837  kur14lem9  27071  heibor1lem  28679  heibor  28691  idlval  28784  mzpclval  29032  eldiophb  29066  rpnnen3  29352  dfac11  29386  rgspnval  29496  lincop  30873  bj-snglex  32366  psubspset  33281  paddfval  33334  pclfvalN  33426  polfvalN  33441  psubclsetN  33473  docafvalN  34660  djafvalN  34672  dicval  34714  dochfval  34888  djhfval  34935  islpolN  35021