MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwexg Unicode version

Theorem pwexg 4196
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.
StepHypRef Expression
1 pweq 3630 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2351 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2793 . . 3  |-  x  e. 
_V
43pwex 4195 . 2  |-  ~P x  e.  _V
52, 4vtoclg 2845 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    e. wcel 1686   _Vcvv 2790   ~Pcpw 3627
This theorem is referenced by:  abssexg  4197  snexALT  4198  pwel  4227  uniexb  4565  xpexg  4802  fabexg  5424  undefval  6303  mapex  6780  pmvalg  6785  pw2eng  6970  fopwdom  6972  pwdom  7015  2pwne  7019  disjen  7020  domss2  7022  ssenen  7037  fineqvlem  7079  fival  7168  fipwuni  7181  hartogslem2  7260  wdompwdom  7294  harwdom  7306  tskwe  7585  ween  7664  acni  7674  acnnum  7681  infpwfien  7691  pwcda1  7822  ackbij1b  7867  fictb  7873  fin2i  7923  isfin2-2  7947  ssfin3ds  7958  fin23lem32  7972  fin23lem39  7978  fin23lem41  7980  isfin1-3  8014  fin1a2lem12  8039  canth3  8185  ondomon  8187  canthnum  8273  canthwe  8275  canthp1lem2  8277  gchxpidm  8293  gchhar  8295  gchpwdom  8298  wrdexg  11427  hashbcval  13051  restid2  13337  prdsplusg  13360  prdsmulr  13361  prdsvsca  13362  ismre  13494  isacs1i  13561  sscpwex  13694  fpwipodrs  14269  acsdrscl  14275  sylow2a  14932  opsrval  16218  istps3OLD  16662  tgdom  16718  distop  16735  fctop  16743  cctop  16745  ppttop  16746  epttop  16748  cldval  16762  ntrfval  16763  clsfval  16764  mretopd  16831  neifval  16838  neif  16839  neival  16841  lpfval  16872  restfpw  16912  ordtbaslem  16920  kgenval  17232  dfac14lem  17313  qtopval  17388  isfbas  17526  fbssfi  17534  fsubbas  17564  fgval  17567  filssufil  17609  hauspwpwf1  17684  hauspwpwdom  17685  flimfnfcls  17725  ptcmplem1  17748  tsmsfbas  17812  eltsms  17817  blfval  17949  issubgo  20972  sigaex  23472  sigaval  23473  pwsiga  23493  indv  23598  coinflipspace  23683  iscvm  23792  cvmsval  23799  altxpexg  24514  hfpw  24817  iscst1  25185  qusp  25553  efilcp  25563  islimrs  25591  lemindclsbu  26006  islocfin  26307  neibastop2lem  26320  fnemeet2  26327  fnejoin1  26328  elrfi  26780  elrfirn  26781  kelac2  27174
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-pow 4190
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168  df-pw 3629
  Copyright terms: Public domain W3C validator