Theorem pwexg 4471

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 3858	. . 3 |- ( x = A -> ~P x = ~P A )
2	1	eleq1d 2504	. 2 |- ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3		vex 2970	. . 3 |- x e. _V
4	3	pwex 4470	. 2 |- ~P x e. _V
5	2, 4	vtoclg 3025	1 |- ( A e. V -> ~P A e. _V )

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   _Vcvv 2967   ~Pcpw 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-pow 4465

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2969  df-in 3330  df-ss 3337  df-pw 3857

This theorem is referenced by:  abssexg  4472  snexALT  4473  pwel  4539  uniexb  6381  xpexg  6502  fabexg  6528  undefval  6787  mapex  7212  pmvalg  7217  pw2eng  7409  fopwdom  7411  pwdom  7455  2pwne  7459  disjen  7460  domss2  7462  ssenen  7477  fineqvlem  7519  fival  7654  fipwuni  7668  hartogslem2  7749  wdompwdom  7785  harwdom  7797  tskwe  8112  ween  8197  acni  8207  acnnum  8214  infpwfien  8224  pwcda1  8355  ackbij1b  8400  fictb  8406  fin2i  8456  isfin2-2  8480  ssfin3ds  8491  fin23lem32  8505  fin23lem39  8511  fin23lem41  8513  isfin1-3  8547  fin1a2lem12  8572  canth3  8717  ondomon  8719  canthnum  8808  canthwe  8810  canthp1lem2  8812  gchxpidm  8828  gchpwdom  8829  gchhar  8838  wrdexg  12236  hashbcval  14055  restid2  14361  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  ismre  14520  isacs1i  14587  sscpwex  14720  fpwipodrs  15326  acsdrscl  15332  sylow2a  16109  opsrval  17536  istps3OLD  18507  tgdom  18563  distop  18580  fctop  18588  cctop  18590  ppttop  18591  epttop  18593  cldval  18607  ntrfval  18608  clsfval  18609  mretopd  18676  neifval  18683  neif  18684  neival  18686  neiptoptop  18715  lpfval  18722  restfpw  18763  ordtbaslem  18772  kgenval  19088  dfac14lem  19170  qtopval  19248  isfbas  19382  fbssfi  19390  fsubbas  19420  fgval  19423  filssufil  19465  hauspwpwf1  19540  hauspwpwdom  19541  flimfnfcls  19581  ptcmplem1  19604  tsmsfbas  19678  eltsms  19683  ustval  19757  isust  19758  utopval  19787  blfvalps  19938  cusgraexilem1  23342  issubgo  23758  indv  26438  sigaex  26521  sigaval  26522  pwsiga  26542  omsval  26677  omsfval  26678  coinflipspace  26832  iscvm  27117  cvmsval  27124  altxpexg  27978  hfpw  28192  islocfin  28539  neibastop2lem  28552  fnemeet2  28559  fnejoin1  28560  elrfi  29001  elrfirn  29002  kelac2  29389