Theorem pwexg 4621

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 4000	. . 3 |- ( x = A -> ~P x = ~P A )
2	1	eleq1d 2512	. 2 |- ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3		vex 3098	. . 3 |- x e. _V
4	3	pwex 4620	. 2 |- ~P x e. _V
5	2, 4	vtoclg 3153	1 |- ( A e. V -> ~P A e. _V )

Syntax hints:   -> wi 4   = wceq 1383   e. wcel 1804   _Vcvv 3095   ~Pcpw 3997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-pow 4615

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097  df-in 3468  df-ss 3475  df-pw 3999

This theorem is referenced by:  abssexg  4622  snexALT  4623  pwel  4689  xpexg  6587  uniexb  6595  fabexg  6741  undefval  7007  mapex  7428  pmvalg  7433  pw2eng  7625  fopwdom  7627  pwdom  7671  2pwne  7675  disjen  7676  domss2  7678  ssenen  7693  fineqvlem  7736  fival  7874  fipwuni  7888  hartogslem2  7971  wdompwdom  8007  harwdom  8019  tskwe  8334  ween  8419  acni  8429  acnnum  8436  infpwfien  8446  pwcda1  8577  ackbij1b  8622  fictb  8628  fin2i  8678  isfin2-2  8702  ssfin3ds  8713  fin23lem32  8727  fin23lem39  8733  fin23lem41  8735  isfin1-3  8769  fin1a2lem12  8794  canth3  8939  ondomon  8941  canthnum  9030  canthwe  9032  canthp1lem2  9034  gchxpidm  9050  gchpwdom  9051  gchhar  9060  wrdexg  12536  hashbcval  14397  restid2  14705  prdsplusg  14732  prdsmulr  14733  prdsvsca  14734  ismre  14864  isacs1i  14931  sscpwex  15061  fpwipodrs  15668  acsdrscl  15674  sylow2a  16513  opsrval  18013  istps3OLD  19296  tgdom  19353  distop  19370  fctop  19378  cctop  19380  ppttop  19381  epttop  19383  cldval  19397  ntrfval  19398  clsfval  19399  mretopd  19466  neifval  19473  neif  19474  neival  19476  neiptoptop  19505  lpfval  19512  restfpw  19553  ordtbaslem  19562  islocfin  19891  dissnref  19902  kgenval  19909  dfac14lem  19991  qtopval  20069  isfbas  20203  fbssfi  20211  fsubbas  20241  fgval  20244  filssufil  20286  hauspwpwf1  20361  hauspwpwdom  20362  flimfnfcls  20402  ptcmplem1  20425  tsmsfbas  20499  eltsms  20504  ustval  20578  isust  20579  utopval  20608  blfvalps  20759  cusgraexilem1  24338  issubgo  25177  indv  27899  sigaex  27982  sigaval  27983  pwsiga  28003  omsval  28137  omsfval  28138  coinflipspace  28292  iscvm  28577  cvmsval  28584  altxpexg  29603  hfpw  29817  neibastop2lem  30153  fnemeet2  30160  fnejoin1  30161  elrfi  30601  elrfirn  30602  kelac2  30986