Theorem pwex 4589

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 3956	. . 3 |- ( z = A -> ~P z = ~P A )
3	2	eleq1d 2515	. 2 |- ( z = A -> ( ~P z e. _V <-> ~P A e. _V ) )
4		df-pw 3955	. . 3 |- ~P z = { y | y C_ z }
5		axpow2 4586	. . . . . 6 |- E. x A. y ( y C_ z -> y e. x )
6	5	bm1.3ii 4531	. . . . 5 |- E. x A. y ( y e. x <-> y C_ z )
7		abeq2 2562	. . . . . 6 |- ( x = { y | y C_ z } <-> A. y ( y e. x <-> y C_ z ) )
8	7	exbii 1720	. . . . 5 |- ( E. x x = { y | y C_ z } <-> E. x A. y ( y e. x <-> y C_ z ) )
9	6, 8	mpbir 213	. . . 4 |- E. x x = { y | y C_ z }
10	9	issetri 3054	. . 3 |- { y | y C_ z } e. _V
11	4, 10	eqeltri 2527	. 2 |- ~P z e. _V
12	1, 3, 11	vtocl 3102	1 |- ~P A e. _V

Syntax hints:   <-> wb 188   A.wal 1444   = wceq 1446   E.wex 1665   e. wcel 1889   {cab 2439   _Vcvv 3047   C_ wss 3406   ~Pcpw 3953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-pow 4584

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3049  df-in 3413  df-ss 3420  df-pw 3955

This theorem is referenced by:  pwexg  4590  p0ex  4593  pp0ex  4595  ord3ex  4596  abexssex  6780  fnpm  7485  canth2  7730  dffi3  7950  inf3lem7  8144  r1sucg  8245  r1pwALT  8322  rankuni  8339  rankc2  8347  rankxpu  8352  rankmapu  8354  rankxplim  8355  r0weon  8448  aceq3lem  8556  dfac5lem4  8562  dfac2a  8565  dfac2  8566  dfac8  8570  dfac13  8577  ackbij1lem5  8659  ackbij1lem8  8662  ackbij2lem2  8675  ackbij2lem3  8676  fin23lem17  8773  domtriomlem  8877  dominf  8880  axdc2lem  8883  axdc3lem  8885  numthcor  8929  axdclem2  8955  alephsucpw  9000  dominfac  9003  canthp1lem1  9082  gchac  9111  intwun  9165  wunex2  9168  eltsk2g  9181  inttsk  9204  tskcard  9211  intgru  9244  gruina  9248  axgroth6  9258  npex  9416  axcnex  9576  pnfxr  11419  mnfxr  11421  ixxex  11653  prdsval  15365  prdsds  15374  prdshom  15377  ismre  15508  fnmre  15509  fnmrc  15525  mrcfval  15526  mrisval  15548  mreacs  15576  wunfunc  15816  catcfuccl  16016  catcxpccl  16104  lubfval  16236  glbfval  16249  isacs5lem  16427  issubm  16606  issubg  16829  cntzfval  16986  pmtrfval  17103  sylow1lem2  17263  lsmfval  17302  pj1fval  17356  issubrg  18020  lssset  18169  lspfval  18208  islbs  18311  lbsext  18398  lbsexg  18399  sraval  18411  aspval  18564  ocvfval  19241  cssval  19257  isobs  19295  islinds  19379  istopon  19952  tgdom  20006  fncld  20049  leordtval2  20240  cnpfval  20262  iscnp2  20267  kgenf  20568  xkoopn  20616  xkouni  20626  dfac14  20645  xkoccn  20646  prdstopn  20655  xkoco1cn  20684  xkoco2cn  20685  xkococn  20687  xkoinjcn  20714  isfbas  20856  uzrest  20924  acufl  20944  alexsubALTlem2  21075  tsmsval2  21156  ustfn  21228  ustn0  21247  ishtpy  22015  vitali  22583  sspval  26374  shex  26877  hsupval  26999  fpwrelmap  28330  fpwrelmapffs  28331  isrnsigaOLD  28946  dmvlsiga  28963  eulerpartlem1  29212  eulerpartgbij  29217  eulerpartlemmf  29220  coinflippv  29328  ballotlemoex  29330  kur14lem9  29949  mpstval  30185  mclsrcl  30211  mclsval  30213  bj-snglex  31579  heibor1lem  32153  heibor  32165  idlval  32258  psubspset  33321  paddfval  33374  pclfvalN  33466  polfvalN  33481  psubclsetN  33513  docafvalN  34702  djafvalN  34714  dicval  34756  dochfval  34930  djhfval  34977  islpolN  35063  mzpclval  35579  eldiophb  35611  rpnnen3  35899  dfac11  35932  rgspnval  36046  pwinfi  36180  ovnval  38372  usgsizedg  39811  usgsizedgALT  39812  usgsizedgALT2  39813  issubmgm  39893  lincop  40305