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

Theorem pwexg 4194
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 3628 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2349 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2791 . . 3  |-  x  e. 
_V
43pwex 4193 . 2  |-  ~P x  e.  _V
52, 4vtoclg 2843 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   _Vcvv 2788   ~Pcpw 3625
This theorem is referenced by:  abssexg  4195  snexALT  4196  pwel  4225  uniexb  4563  xpexg  4800  fabexg  5422  undefval  6301  mapex  6778  pmvalg  6783  pw2eng  6968  fopwdom  6970  pwdom  7013  2pwne  7017  disjen  7018  domss2  7020  ssenen  7035  fineqvlem  7077  fival  7166  fipwuni  7179  hartogslem2  7258  wdompwdom  7292  harwdom  7304  tskwe  7583  ween  7662  acni  7672  acnnum  7679  infpwfien  7689  pwcda1  7820  ackbij1b  7865  fictb  7871  fin2i  7921  isfin2-2  7945  ssfin3ds  7956  fin23lem32  7970  fin23lem39  7976  fin23lem41  7978  isfin1-3  8012  fin1a2lem12  8037  canth3  8183  ondomon  8185  canthnum  8271  canthwe  8273  canthp1lem2  8275  gchxpidm  8291  gchhar  8293  gchpwdom  8296  wrdexg  11425  hashbcval  13049  restid2  13335  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  ismre  13492  isacs1i  13559  sscpwex  13692  fpwipodrs  14267  acsdrscl  14273  sylow2a  14930  opsrval  16216  istps3OLD  16660  tgdom  16716  distop  16733  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  cldval  16760  ntrfval  16761  clsfval  16762  mretopd  16829  neifval  16836  neif  16837  neival  16839  lpfval  16870  restfpw  16910  ordtbaslem  16918  kgenval  17230  dfac14lem  17311  qtopval  17386  isfbas  17524  fbssfi  17532  fsubbas  17562  fgval  17565  filssufil  17607  hauspwpwf1  17682  hauspwpwdom  17683  flimfnfcls  17723  ptcmplem1  17746  tsmsfbas  17810  eltsms  17815  blfval  17947  issubgo  20970  sigaex  23470  sigaval  23471  pwsiga  23491  indv  23596  coinflipspace  23681  iscvm  23790  cvmsval  23797  altxpexg  24512  hfpw  24815  iscst1  25174  qusp  25542  efilcp  25552  islimrs  25580  lemindclsbu  25995  islocfin  26296  neibastop2lem  26309  fnemeet2  26316  fnejoin1  26317  elrfi  26769  elrfirn  26770  kelac2  27163
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-pow 4188
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator