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

Theorem pwexg 4210
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 3641 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2362 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2804 . . 3  |-  x  e. 
_V
43pwex 4209 . 2  |-  ~P x  e.  _V
52, 4vtoclg 2856 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   _Vcvv 2801   ~Pcpw 3638
This theorem is referenced by:  abssexg  4211  snexALT  4212  pwel  4241  uniexb  4579  xpexg  4816  fabexg  5438  undefval  6317  mapex  6794  pmvalg  6799  pw2eng  6984  fopwdom  6986  pwdom  7029  2pwne  7033  disjen  7034  domss2  7036  ssenen  7051  fineqvlem  7093  fival  7182  fipwuni  7195  hartogslem2  7274  wdompwdom  7308  harwdom  7320  tskwe  7599  ween  7678  acni  7688  acnnum  7695  infpwfien  7705  pwcda1  7836  ackbij1b  7881  fictb  7887  fin2i  7937  isfin2-2  7961  ssfin3ds  7972  fin23lem32  7986  fin23lem39  7992  fin23lem41  7994  isfin1-3  8028  fin1a2lem12  8053  canth3  8199  ondomon  8201  canthnum  8287  canthwe  8289  canthp1lem2  8291  gchxpidm  8307  gchhar  8309  gchpwdom  8312  wrdexg  11441  hashbcval  13065  restid2  13351  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  ismre  13508  isacs1i  13575  sscpwex  13708  fpwipodrs  14283  acsdrscl  14289  sylow2a  14946  opsrval  16232  istps3OLD  16676  tgdom  16732  distop  16749  fctop  16757  cctop  16759  ppttop  16760  epttop  16762  cldval  16776  ntrfval  16777  clsfval  16778  mretopd  16845  neifval  16852  neif  16853  neival  16855  lpfval  16886  restfpw  16926  ordtbaslem  16934  kgenval  17246  dfac14lem  17327  qtopval  17402  isfbas  17540  fbssfi  17548  fsubbas  17578  fgval  17581  filssufil  17623  hauspwpwf1  17698  hauspwpwdom  17699  flimfnfcls  17739  ptcmplem1  17762  tsmsfbas  17826  eltsms  17831  blfval  17963  issubgo  20986  sigaex  23485  sigaval  23486  pwsiga  23506  indv  23611  coinflipspace  23696  iscvm  23805  cvmsval  23812  altxpexg  24584  hfpw  24887  iscst1  25277  qusp  25645  efilcp  25655  islimrs  25683  lemindclsbu  26098  islocfin  26399  neibastop2lem  26412  fnemeet2  26419  fnejoin1  26420  elrfi  26872  elrfirn  26873  kelac2  27266
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-pow 4204
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640
  Copyright terms: Public domain W3C validator