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

Theorem pwexg 4324
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 3745 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2453 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2902 . . 3  |-  x  e. 
_V
43pwex 4323 . 2  |-  ~P x  e.  _V
52, 4vtoclg 2954 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   _Vcvv 2899   ~Pcpw 3742
This theorem is referenced by:  abssexg  4325  snexALT  4326  pwel  4356  uniexb  4692  xpexg  4929  fabexg  5564  undefval  6482  mapex  6960  pmvalg  6965  pw2eng  7150  fopwdom  7152  pwdom  7195  2pwne  7199  disjen  7200  domss2  7202  ssenen  7217  fineqvlem  7259  fival  7352  fipwuni  7366  hartogslem2  7445  wdompwdom  7479  harwdom  7491  tskwe  7770  ween  7849  acni  7859  acnnum  7866  infpwfien  7876  pwcda1  8007  ackbij1b  8052  fictb  8058  fin2i  8108  isfin2-2  8132  ssfin3ds  8143  fin23lem32  8157  fin23lem39  8163  fin23lem41  8165  isfin1-3  8199  fin1a2lem12  8224  canth3  8369  ondomon  8371  canthnum  8457  canthwe  8459  canthp1lem2  8461  gchxpidm  8477  gchhar  8479  gchpwdom  8482  wrdexg  11666  hashbcval  13297  restid2  13585  prdsplusg  13608  prdsmulr  13609  prdsvsca  13610  ismre  13742  isacs1i  13809  sscpwex  13942  fpwipodrs  14517  acsdrscl  14523  sylow2a  15180  opsrval  16462  istps3OLD  16910  tgdom  16966  distop  16983  fctop  16991  cctop  16993  ppttop  16994  epttop  16996  cldval  17010  ntrfval  17011  clsfval  17012  mretopd  17079  neifval  17086  neif  17087  neival  17089  neiptoptop  17118  lpfval  17125  restfpw  17165  ordtbaslem  17174  kgenval  17488  dfac14lem  17570  qtopval  17648  isfbas  17782  fbssfi  17790  fsubbas  17820  fgval  17823  filssufil  17865  hauspwpwf1  17940  hauspwpwdom  17941  flimfnfcls  17981  ptcmplem1  18004  tsmsfbas  18078  eltsms  18083  ustval  18153  isust  18154  utopval  18183  blfval  18321  cusgraexilem1  21341  issubgo  21739  indv  24206  sigaex  24288  sigaval  24289  pwsiga  24309  coinflipspace  24517  iscvm  24725  cvmsval  24732  altxpexg  25537  hfpw  25840  islocfin  26067  neibastop2lem  26080  fnemeet2  26087  fnejoin1  26088  elrfi  26439  elrfirn  26440  kelac2  26832
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 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-pow 4318
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-ss 3277  df-pw 3744
  Copyright terms: Public domain W3C validator