Theorem pwexg 4574

Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.)

Assertion

Ref	Expression
pwexg	|- ( A e. V -> ~P A e. _V )

Proof of Theorem pwexg

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pweq 3961	. . 3 |- ( x = A -> ~P x = ~P A )
2	1	eleq1d 2520	. 2 |- ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3		vex 3071	. . 3 |- x e. _V
4	3	pwex 4573	. 2 |- ~P x e. _V
5	2, 4	vtoclg 3126	1 |- ( A e. V -> ~P A e. _V )

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758   _Vcvv 3068   ~Pcpw 3958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-pow 4568

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3070  df-in 3433  df-ss 3440  df-pw 3960

This theorem is referenced by:  abssexg  4575  snexALT  4576  pwel  4642  uniexb  6486  xpexg  6607  fabexg  6633  undefval  6895  mapex  7320  pmvalg  7325  pw2eng  7517  fopwdom  7519  pwdom  7563  2pwne  7567  disjen  7568  domss2  7570  ssenen  7585  fineqvlem  7628  fival  7763  fipwuni  7777  hartogslem2  7858  wdompwdom  7894  harwdom  7906  tskwe  8221  ween  8306  acni  8316  acnnum  8323  infpwfien  8333  pwcda1  8464  ackbij1b  8509  fictb  8515  fin2i  8565  isfin2-2  8589  ssfin3ds  8600  fin23lem32  8614  fin23lem39  8620  fin23lem41  8622  isfin1-3  8656  fin1a2lem12  8681  canth3  8826  ondomon  8828  canthnum  8917  canthwe  8919  canthp1lem2  8921  gchxpidm  8937  gchpwdom  8938  gchhar  8947  wrdexg  12346  hashbcval  14165  restid2  14471  prdsplusg  14498  prdsmulr  14499  prdsvsca  14500  ismre  14630  isacs1i  14697  sscpwex  14830  fpwipodrs  15436  acsdrscl  15442  sylow2a  16222  opsrval  17663  istps3OLD  18643  tgdom  18699  distop  18716  fctop  18724  cctop  18726  ppttop  18727  epttop  18729  cldval  18743  ntrfval  18744  clsfval  18745  mretopd  18812  neifval  18819  neif  18820  neival  18822  neiptoptop  18851  lpfval  18858  restfpw  18899  ordtbaslem  18908  kgenval  19224  dfac14lem  19306  qtopval  19384  isfbas  19518  fbssfi  19526  fsubbas  19556  fgval  19559  filssufil  19601  hauspwpwf1  19676  hauspwpwdom  19677  flimfnfcls  19717  ptcmplem1  19740  tsmsfbas  19814  eltsms  19819  ustval  19893  isust  19894  utopval  19923  blfvalps  20074  cusgraexilem1  23509  issubgo  23925  indv  26603  sigaex  26686  sigaval  26687  pwsiga  26707  omsval  26842  omsfval  26843  coinflipspace  26997  iscvm  27282  cvmsval  27289  altxpexg  28143  hfpw  28357  islocfin  28706  neibastop2lem  28719  fnemeet2  28726  fnejoin1  28727  elrfi  29168  elrfirn  29169  kelac2  29556