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

Theorem pwexg 4347
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 3766 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2474 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2923 . . 3  |-  x  e. 
_V
43pwex 4346 . 2  |-  ~P x  e.  _V
52, 4vtoclg 2975 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   _Vcvv 2920   ~Pcpw 3763
This theorem is referenced by:  abssexg  4348  snexALT  4349  pwel  4379  uniexb  4715  xpexg  4952  fabexg  5587  undefval  6509  mapex  6987  pmvalg  6992  pw2eng  7177  fopwdom  7179  pwdom  7222  2pwne  7226  disjen  7227  domss2  7229  ssenen  7244  fineqvlem  7286  fival  7379  fipwuni  7393  hartogslem2  7472  wdompwdom  7506  harwdom  7518  tskwe  7797  ween  7876  acni  7886  acnnum  7893  infpwfien  7903  pwcda1  8034  ackbij1b  8079  fictb  8085  fin2i  8135  isfin2-2  8159  ssfin3ds  8170  fin23lem32  8184  fin23lem39  8190  fin23lem41  8192  isfin1-3  8226  fin1a2lem12  8251  canth3  8396  ondomon  8398  canthnum  8484  canthwe  8486  canthp1lem2  8488  gchxpidm  8504  gchhar  8506  gchpwdom  8509  wrdexg  11698  hashbcval  13329  restid2  13617  prdsplusg  13640  prdsmulr  13641  prdsvsca  13642  ismre  13774  isacs1i  13841  sscpwex  13974  fpwipodrs  14549  acsdrscl  14555  sylow2a  15212  opsrval  16494  istps3OLD  16946  tgdom  17002  distop  17019  fctop  17027  cctop  17029  ppttop  17030  epttop  17032  cldval  17046  ntrfval  17047  clsfval  17048  mretopd  17115  neifval  17122  neif  17123  neival  17125  neiptoptop  17154  lpfval  17161  restfpw  17201  ordtbaslem  17210  kgenval  17524  dfac14lem  17606  qtopval  17684  isfbas  17818  fbssfi  17826  fsubbas  17856  fgval  17859  filssufil  17901  hauspwpwf1  17976  hauspwpwdom  17977  flimfnfcls  18017  ptcmplem1  18040  tsmsfbas  18114  eltsms  18119  ustval  18189  isust  18190  utopval  18219  blfvalps  18370  cusgraexilem1  21432  issubgo  21848  indv  24367  sigaex  24449  sigaval  24450  pwsiga  24470  coinflipspace  24695  iscvm  24903  cvmsval  24910  altxpexg  25731  hfpw  26034  islocfin  26270  neibastop2lem  26283  fnemeet2  26290  fnejoin1  26291  elrfi  26642  elrfirn  26643  kelac2  27035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-pow 4341
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-in 3291  df-ss 3298  df-pw 3765
  Copyright terms: Public domain W3C validator