Theorem pwexg 4624

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 4006	. . 3 |- ( x = A -> ~P x = ~P A )
2	1	eleq1d 2529	. 2 |- ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3		vex 3109	. . 3 |- x e. _V
4	3	pwex 4623	. 2 |- ~P x e. _V
5	2, 4	vtoclg 3164	1 |- ( A e. V -> ~P A e. _V )

Syntax hints:   -> wi 4   = wceq 1374   e. wcel 1762   _Vcvv 3106   ~Pcpw 4003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-pow 4618

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-v 3108  df-in 3476  df-ss 3483  df-pw 4005

This theorem is referenced by:  abssexg  4625  snexALT  4626  pwel  4692  uniexb  6581  xpexg  6702  fabexg  6730  undefval  6995  mapex  7416  pmvalg  7421  pw2eng  7613  fopwdom  7615  pwdom  7659  2pwne  7663  disjen  7664  domss2  7666  ssenen  7681  fineqvlem  7724  fival  7861  fipwuni  7875  hartogslem2  7957  wdompwdom  7993  harwdom  8005  tskwe  8320  ween  8405  acni  8415  acnnum  8422  infpwfien  8432  pwcda1  8563  ackbij1b  8608  fictb  8614  fin2i  8664  isfin2-2  8688  ssfin3ds  8699  fin23lem32  8713  fin23lem39  8719  fin23lem41  8721  isfin1-3  8755  fin1a2lem12  8780  canth3  8925  ondomon  8927  canthnum  9016  canthwe  9018  canthp1lem2  9020  gchxpidm  9036  gchpwdom  9037  gchhar  9046  wrdexg  12510  hashbcval  14368  restid2  14675  prdsplusg  14702  prdsmulr  14703  prdsvsca  14704  ismre  14834  isacs1i  14901  sscpwex  15034  fpwipodrs  15640  acsdrscl  15646  sylow2a  16428  opsrval  17903  istps3OLD  19183  tgdom  19239  distop  19256  fctop  19264  cctop  19266  ppttop  19267  epttop  19269  cldval  19283  ntrfval  19284  clsfval  19285  mretopd  19352  neifval  19359  neif  19360  neival  19362  neiptoptop  19391  lpfval  19398  restfpw  19439  ordtbaslem  19448  kgenval  19764  dfac14lem  19846  qtopval  19924  isfbas  20058  fbssfi  20066  fsubbas  20096  fgval  20099  filssufil  20141  hauspwpwf1  20216  hauspwpwdom  20217  flimfnfcls  20257  ptcmplem1  20280  tsmsfbas  20354  eltsms  20359  ustval  20433  isust  20434  utopval  20463  blfvalps  20614  cusgraexilem1  24128  issubgo  24831  indv  27516  sigaex  27599  sigaval  27600  pwsiga  27620  omsval  27754  omsfval  27755  coinflipspace  27909  iscvm  28194  cvmsval  28201  altxpexg  29055  hfpw  29269  islocfin  29619  neibastop2lem  29632  fnemeet2  29639  fnejoin1  29640  elrfi  30081  elrfirn  30082  kelac2  30468