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

Theorem pwexg 4193
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 3629 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2350 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2792 . . 3  |-  x  e. 
_V
43pwex 4192 . 2  |-  ~P x  e.  _V
52, 4vtoclg 2844 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1685   _Vcvv 2789   ~Pcpw 3626
This theorem is referenced by:  abssexg  4194  snexALT  4195  pwel  4224  uniexb  4562  xpexg  4799  fabexg  5388  undefval  6297  mapex  6774  pmvalg  6779  pw2eng  6964  fopwdom  6966  pwdom  7009  2pwne  7013  disjen  7014  domss2  7016  ssenen  7031  fineqvlem  7073  fival  7162  fipwuni  7175  hartogslem2  7254  wdompwdom  7288  harwdom  7300  tskwe  7579  ween  7658  acni  7668  acnnum  7675  infpwfien  7685  pwcda1  7816  ackbij1b  7861  fictb  7867  fin2i  7917  isfin2-2  7941  ssfin3ds  7952  fin23lem32  7966  fin23lem39  7972  fin23lem41  7974  isfin1-3  8008  fin1a2lem12  8033  canth3  8179  ondomon  8181  canthnum  8267  canthwe  8269  canthp1lem2  8271  gchxpidm  8287  gchhar  8289  gchpwdom  8292  wrdexg  11421  hashbcval  13045  restid2  13331  prdsplusg  13354  prdsmulr  13355  prdsvsca  13356  ismre  13488  isacs1i  13555  sscpwex  13688  fpwipodrs  14263  acsdrscl  14269  sylow2a  14926  opsrval  16212  istps3OLD  16656  tgdom  16712  distop  16729  fctop  16737  cctop  16739  ppttop  16740  epttop  16742  cldval  16756  ntrfval  16757  clsfval  16758  mretopd  16825  neifval  16832  neif  16833  neival  16835  lpfval  16866  restfpw  16906  ordtbaslem  16914  kgenval  17226  dfac14lem  17307  qtopval  17382  isfbas  17520  fbssfi  17528  fsubbas  17558  fgval  17561  filssufil  17603  hauspwpwf1  17678  hauspwpwdom  17679  flimfnfcls  17719  ptcmplem1  17742  tsmsfbas  17806  eltsms  17811  blfval  17943  issubgo  20964  iscvm  23197  cvmsval  23204  altxpexg  23922  hfpw  24225  iscst1  24585  qusp  24953  efilcp  24963  islimrs  24991  lemindclsbu  25406  islocfin  25707  neibastop2lem  25720  fnemeet2  25727  fnejoin1  25728  elrfi  26180  elrfirn  26181  kelac2  26574
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 1636  ax-8 1644  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-pow 4187
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-pw 3628
  Copyright terms: Public domain W3C validator