Theorem pwex 4603

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 3982	. . 3 |- ( z = A -> ~P z = ~P A )
3	2	eleq1d 2491	. 2 |- ( z = A -> ( ~P z e. _V <-> ~P A e. _V ) )
4		df-pw 3981	. . 3 |- ~P z = { y | y C_ z }
5		axpow2 4600	. . . . . 6 |- E. x A. y ( y C_ z -> y e. x )
6	5	bm1.3ii 4546	. . . . 5 |- E. x A. y ( y e. x <-> y C_ z )
7		abeq2 2546	. . . . . 6 |- ( x = { y | y C_ z } <-> A. y ( y e. x <-> y C_ z ) )
8	7	exbii 1712	. . . . 5 |- ( E. x x = { y | y C_ z } <-> E. x A. y ( y e. x <-> y C_ z ) )
9	6, 8	mpbir 212	. . . 4 |- E. x x = { y | y C_ z }
10	9	issetri 3088	. . 3 |- { y | y C_ z } e. _V
11	4, 10	eqeltri 2506	. 2 |- ~P z e. _V
12	1, 3, 11	vtocl 3133	1 |- ~P A e. _V

Syntax hints:   <-> wb 187   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1868   {cab 2407   _Vcvv 3081   C_ wss 3436   ~Pcpw 3979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-pow 4598

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-v 3083  df-in 3443  df-ss 3450  df-pw 3981

This theorem is referenced by:  pwexg  4604  p0ex  4607  pp0ex  4609  ord3ex  4610  abexssex  6785  fnpm  7484  canth2  7727  dffi3  7947  inf3lem7  8141  r1sucg  8241  r1pwALT  8318  rankuni  8335  rankc2  8343  rankxpu  8348  rankmapu  8350  rankxplim  8351  r0weon  8444  aceq3lem  8551  dfac5lem4  8557  dfac2a  8560  dfac2  8561  dfac8  8565  dfac13  8572  ackbij1lem5  8654  ackbij1lem8  8657  ackbij2lem2  8670  ackbij2lem3  8671  fin23lem17  8768  domtriomlem  8872  dominf  8875  axdc2lem  8878  axdc3lem  8880  numthcor  8924  axdclem2  8950  alephsucpw  8995  dominfac  8998  canthp1lem1  9077  gchac  9106  intwun  9160  wunex2  9163  eltsk2g  9176  inttsk  9199  tskcard  9206  intgru  9239  gruina  9243  axgroth6  9253  npex  9411  axcnex  9571  pnfxr  11412  mnfxr  11414  ixxex  11646  prdsval  15340  prdsds  15349  prdshom  15352  ismre  15483  fnmre  15484  fnmrc  15500  mrcfval  15501  mrisval  15523  mreacs  15551  wunfunc  15791  catcfuccl  15991  catcxpccl  16079  lubfval  16211  glbfval  16224  isacs5lem  16402  issubm  16581  issubg  16804  cntzfval  16961  pmtrfval  17078  sylow1lem2  17238  lsmfval  17277  pj1fval  17331  issubrg  17995  lssset  18144  lspfval  18183  islbs  18286  lbsext  18373  lbsexg  18374  sraval  18386  aspval  18539  ocvfval  19215  cssval  19231  isobs  19269  islinds  19353  istopon  19926  tgdom  19980  fncld  20023  leordtval2  20214  cnpfval  20236  iscnp2  20241  kgenf  20542  xkoopn  20590  xkouni  20600  dfac14  20619  xkoccn  20620  prdstopn  20629  xkoco1cn  20658  xkoco2cn  20659  xkococn  20661  xkoinjcn  20688  isfbas  20830  uzrest  20898  acufl  20918  alexsubALTlem2  21049  tsmsval2  21130  ustfn  21202  ustn0  21221  ishtpy  21989  vitali  22557  sspval  26347  shex  26850  hsupval  26972  fpwrelmap  28311  fpwrelmapffs  28312  isrnsigaOLD  28929  dmvlsiga  28946  eulerpartlem1  29195  eulerpartgbij  29200  eulerpartlemmf  29203  coinflippv  29311  ballotlemoex  29313  kur14lem9  29932  mpstval  30168  mclsrcl  30194  mclsval  30196  bj-snglex  31522  heibor1lem  32054  heibor  32066  idlval  32159  psubspset  33227  paddfval  33280  pclfvalN  33372  polfvalN  33387  psubclsetN  33419  docafvalN  34608  djafvalN  34620  dicval  34662  dochfval  34836  djhfval  34883  islpolN  34969  mzpclval  35485  eldiophb  35517  rpnnen3  35806  dfac11  35839  rgspnval  35953  pwinfi  36087  ovnval  38136  usgsizedg  38978  usgsizedgALT  38979  usgsizedgALT2  38980  issubmgm  39060  lincop  39474