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

Theorem pwexg 4376
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 3795 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2502 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2952 . . 3  |-  x  e. 
_V
43pwex 4375 . 2  |-  ~P x  e.  _V
52, 4vtoclg 3004 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   _Vcvv 2949   ~Pcpw 3792
This theorem is referenced by:  abssexg  4377  snexALT  4378  pwel  4408  uniexb  4745  xpexg  4982  fabexg  5617  undefval  6539  mapex  7017  pmvalg  7022  pw2eng  7207  fopwdom  7209  pwdom  7252  2pwne  7256  disjen  7257  domss2  7259  ssenen  7274  fineqvlem  7316  fival  7410  fipwuni  7424  hartogslem2  7505  wdompwdom  7539  harwdom  7551  tskwe  7830  ween  7909  acni  7919  acnnum  7926  infpwfien  7936  pwcda1  8067  ackbij1b  8112  fictb  8118  fin2i  8168  isfin2-2  8192  ssfin3ds  8203  fin23lem32  8217  fin23lem39  8223  fin23lem41  8225  isfin1-3  8259  fin1a2lem12  8284  canth3  8429  ondomon  8431  canthnum  8517  canthwe  8519  canthp1lem2  8521  gchxpidm  8537  gchhar  8539  gchpwdom  8542  wrdexg  11732  hashbcval  13363  restid2  13651  prdsplusg  13674  prdsmulr  13675  prdsvsca  13676  ismre  13808  isacs1i  13875  sscpwex  14008  fpwipodrs  14583  acsdrscl  14589  sylow2a  15246  opsrval  16528  istps3OLD  16980  tgdom  17036  distop  17053  fctop  17061  cctop  17063  ppttop  17064  epttop  17066  cldval  17080  ntrfval  17081  clsfval  17082  mretopd  17149  neifval  17156  neif  17157  neival  17159  neiptoptop  17188  lpfval  17195  restfpw  17236  ordtbaslem  17245  kgenval  17560  dfac14lem  17642  qtopval  17720  isfbas  17854  fbssfi  17862  fsubbas  17892  fgval  17895  filssufil  17937  hauspwpwf1  18012  hauspwpwdom  18013  flimfnfcls  18053  ptcmplem1  18076  tsmsfbas  18150  eltsms  18155  ustval  18225  isust  18226  utopval  18255  blfvalps  18406  cusgraexilem1  21468  issubgo  21884  indv  24403  sigaex  24485  sigaval  24486  pwsiga  24506  coinflipspace  24731  iscvm  24939  cvmsval  24946  altxpexg  25816  hfpw  26119  islocfin  26368  neibastop2lem  26381  fnemeet2  26388  fnejoin1  26389  elrfi  26740  elrfirn  26741  kelac2  27132
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4323  ax-pow 4370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951  df-in 3320  df-ss 3327  df-pw 3794
  Copyright terms: Public domain W3C validator