Theorem pwex 4584

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 3945	. . 3 |- ( z = A -> ~P z = ~P A )
3	2	eleq1d 2533	. 2 |- ( z = A -> ( ~P z e. _V <-> ~P A e. _V ) )
4		df-pw 3944	. . 3 |- ~P z = { y | y C_ z }
5		axpow2 4581	. . . . . 6 |- E. x A. y ( y C_ z -> y e. x )
6	5	bm1.3ii 4521	. . . . 5 |- E. x A. y ( y e. x <-> y C_ z )
7		abeq2 2580	. . . . . 6 |- ( x = { y | y C_ z } <-> A. y ( y e. x <-> y C_ z ) )
8	7	exbii 1726	. . . . 5 |- ( E. x x = { y | y C_ z } <-> E. x A. y ( y e. x <-> y C_ z ) )
9	6, 8	mpbir 214	. . . 4 |- E. x x = { y | y C_ z }
10	9	issetri 3038	. . 3 |- { y | y C_ z } e. _V
11	4, 10	eqeltri 2545	. 2 |- ~P z e. _V
12	1, 3, 11	vtocl 3086	1 |- ~P A e. _V

Syntax hints:   <-> wb 189   A.wal 1450   = wceq 1452   E.wex 1671   e. wcel 1904   {cab 2457   _Vcvv 3031   C_ wss 3390   ~Pcpw 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-pow 4579

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-v 3033  df-in 3397  df-ss 3404  df-pw 3944

This theorem is referenced by:  pwexg  4585  p0ex  4588  pp0ex  4590  ord3ex  4591  abexssex  6794  fnpm  7498  canth2  7743  dffi3  7963  inf3lem7  8157  r1sucg  8258  r1pwALT  8335  rankuni  8352  rankc2  8360  rankxpu  8365  rankmapu  8367  rankxplim  8368  r0weon  8461  aceq3lem  8569  dfac5lem4  8575  dfac2a  8578  dfac2  8579  dfac8  8583  dfac13  8590  ackbij1lem5  8672  ackbij1lem8  8675  ackbij2lem2  8688  ackbij2lem3  8689  fin23lem17  8786  domtriomlem  8890  dominf  8893  axdc2lem  8896  axdc3lem  8898  numthcor  8942  axdclem2  8968  alephsucpw  9013  dominfac  9016  canthp1lem1  9095  gchac  9124  intwun  9178  wunex2  9181  eltsk2g  9194  inttsk  9217  tskcard  9224  intgru  9257  gruina  9261  axgroth6  9271  npex  9429  axcnex  9589  pnfxr  11435  mnfxr  11437  ixxex  11671  prdsval  15431  prdsds  15440  prdshom  15443  ismre  15574  fnmre  15575  fnmrc  15591  mrcfval  15592  mrisval  15614  mreacs  15642  wunfunc  15882  catcfuccl  16082  catcxpccl  16170  lubfval  16302  glbfval  16315  isacs5lem  16493  issubm  16672  issubg  16895  cntzfval  17052  pmtrfval  17169  sylow1lem2  17329  lsmfval  17368  pj1fval  17422  issubrg  18086  lssset  18235  lspfval  18274  islbs  18377  lbsext  18464  lbsexg  18465  sraval  18477  aspval  18629  ocvfval  19306  cssval  19322  isobs  19360  islinds  19444  istopon  20017  tgdom  20071  fncld  20114  leordtval2  20305  cnpfval  20327  iscnp2  20332  kgenf  20633  xkoopn  20681  xkouni  20691  dfac14  20710  xkoccn  20711  prdstopn  20720  xkoco1cn  20749  xkoco2cn  20750  xkococn  20752  xkoinjcn  20779  isfbas  20922  uzrest  20990  acufl  21010  alexsubALTlem2  21141  tsmsval2  21222  ustfn  21294  ustn0  21313  ishtpy  22081  vitali  22650  sspval  26443  shex  26946  hsupval  27068  fpwrelmap  28393  fpwrelmapffs  28394  isrnsigaOLD  29008  dmvlsiga  29025  eulerpartlem1  29273  eulerpartgbij  29278  eulerpartlemmf  29281  coinflippv  29389  ballotlemoex  29391  kur14lem9  30009  mpstval  30245  mclsrcl  30271  mclsval  30273  bj-snglex  31637  heibor1lem  32205  heibor  32217  idlval  32310  psubspset  33380  paddfval  33433  pclfvalN  33525  polfvalN  33540  psubclsetN  33572  docafvalN  34761  djafvalN  34773  dicval  34815  dochfval  34989  djhfval  35036  islpolN  35122  mzpclval  35638  eldiophb  35670  rpnnen3  35958  dfac11  35991  rgspnval  36105  pwinfi  36239  dmvolsal  38317  ovnval  38481  usgsizedg  40215  usgsizedgALT  40216  usgsizedgALT2  40217  issubmgm  40297  lincop  40709