Theorem pwex 4342

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 3762	. . 3 |- ( z = A -> ~P z = ~P A )
3	2	eleq1d 2470	. 2 |- ( z = A -> ( ~P z e. _V <-> ~P A e. _V ) )
4		df-pw 3761	. . 3 |- ~P z = { y | y C_ z }
5		axpow2 4339	. . . . . 6 |- E. x A. y ( y C_ z -> y e. x )
6	5	bm1.3ii 4293	. . . . 5 |- E. x A. y ( y e. x <-> y C_ z )
7		abeq2 2509	. . . . . 6 |- ( x = { y | y C_ z } <-> A. y ( y e. x <-> y C_ z ) )
8	7	exbii 1589	. . . . 5 |- ( E. x x = { y | y C_ z } <-> E. x A. y ( y e. x <-> y C_ z ) )
9	6, 8	mpbir 201	. . . 4 |- E. x x = { y | y C_ z }
10	9	issetri 2923	. . 3 |- { y | y C_ z } e. _V
11	4, 10	eqeltri 2474	. 2 |- ~P z e. _V
12	1, 3, 11	vtocl 2966	1 |- ~P A e. _V

Syntax hints:   <-> wb 177   A.wal 1546   E.wex 1547   = wceq 1649   e. wcel 1721   {cab 2390   _Vcvv 2916   C_ wss 3280   ~Pcpw 3759

This theorem is referenced by:  pwexg  4343  p0ex  4346  pp0ex  4348  ord3ex  4349  abexssex  5961  fnpm  6985  canth2  7219  dffi3  7394  inf3lem7  7545  r1sucg  7651  r1pwOLD  7728  rankuni  7745  rankc2  7753  rankxpu  7758  rankxplim  7759  r0weon  7850  aceq3lem  7957  dfac5lem4  7963  dfac2a  7966  dfac2  7967  dfac8  7971  dfac13  7978  ackbij1lem5  8060  ackbij1lem8  8063  ackbij2lem2  8076  ackbij2lem3  8077  fin23lem17  8174  domtriomlem  8278  dominf  8281  axdc2lem  8284  axdc3lem  8286  numthcor  8330  axdclem2  8356  alephsucpw  8401  dominfac  8404  canthp1lem1  8483  gchac  8504  intwun  8566  wunex2  8569  eltsk2g  8582  inttsk  8605  tskcard  8612  intgru  8645  gruina  8649  axgroth6  8659  npex  8819  axcnex  8978  pnfxr  10669  mnfxr  10670  ixxex  10883  prdsval  13633  prdsds  13641  prdshom  13644  ismre  13770  fnmre  13771  fnmrc  13787  mrcfval  13788  mrisval  13810  mreacs  13838  wunfunc  14051  catcfuccl  14219  catcxpccl  14259  lubfval  14390  glbfval  14395  isacs5lem  14550  issubm  14703  issubg  14899  cntzfval  15074  sylow1lem2  15188  lsmfval  15227  pj1fval  15281  issubrg  15823  lssset  15965  lspfval  16004  islbs  16103  lbsext  16190  lbsexg  16191  sraval  16203  aspval  16342  ocvfval  16848  cssval  16864  isobs  16902  istopon  16945  tgdom  16998  fncld  17041  leordtval2  17230  cnpfval  17252  iscnp2  17257  kgenf  17526  xkoopn  17574  xkouni  17584  dfac14  17603  xkoccn  17604  prdstopn  17613  xkoco1cn  17642  xkoco2cn  17643  xkococn  17645  xkoinjcn  17672  isfbas  17814  uzrest  17882  acufl  17902  alexsubALTlem2  18032  tsmsval2  18112  ustfn  18184  ustn0  18203  ishtpy  18950  vitali  19458  sspval  22175  shex  22667  hsupval  22789  isrnsigaOLD  24448  dmvlsiga  24465  coinflippv  24694  ballotlemoex  24696  kur14lem9  24853  heibor1lem  26408  heibor  26420  idlval  26513  mzpclval  26672  eldiophb  26705  rpnnen3  26993  dfac11  27028  islinds  27147  rgspnval  27241  pmtrfval  27261  psubspset  30226  paddfval  30279  pclfvalN  30371  polfvalN  30386  psubclsetN  30418  docafvalN  31605  djafvalN  31617  dicval  31659  dochfval  31833  djhfval  31880  islpolN  31966

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-pow 4337

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761