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

Theorem pwexg 4132
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
StepHypRef Expression
1 pweq 3569 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2322 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2743 . . 3  |-  x  e. 
_V
43pwex 4131 . 2  |-  ~P x  e.  _V
52, 4vtoclg 2794 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   _Vcvv 2740   ~Pcpw 3566
This theorem is referenced by:  abssexg  4133  snexALT  4134  pwel  4163  uniexb  4500  xpexg  4753  fabexg  5325  undefval  6234  mapex  6711  pmvalg  6716  pw2eng  6901  fopwdom  6903  pwdom  6946  2pwne  6950  disjen  6951  domss2  6953  ssenen  6968  fineqvlem  7010  fival  7099  fipwuni  7112  hartogslem2  7191  wdompwdom  7225  harwdom  7237  tskwe  7516  ween  7595  acni  7605  acnnum  7612  infpwfien  7622  pwcda1  7753  ackbij1b  7798  fictb  7804  fin2i  7854  isfin2-2  7878  ssfin3ds  7889  fin23lem32  7903  fin23lem39  7909  fin23lem41  7911  isfin1-3  7945  fin1a2lem12  7970  canth3  8116  ondomon  8118  canthnum  8204  canthwe  8206  canthp1lem2  8208  gchxpidm  8224  gchhar  8226  gchpwdom  8229  wrdexg  11355  hashbcval  12976  restid2  13262  prdsplusg  13285  prdsmulr  13286  prdsvsca  13287  ismre  13419  isacs1i  13486  sscpwex  13619  fpwipodrs  14194  acsdrscl  14200  sylow2a  14857  opsrval  16143  istps3OLD  16587  tgdom  16643  distop  16660  fctop  16668  cctop  16670  ppttop  16671  epttop  16673  cldval  16687  ntrfval  16688  clsfval  16689  mretopd  16756  neifval  16763  neif  16764  neival  16766  lpfval  16797  restfpw  16837  ordtbaslem  16845  kgenval  17157  dfac14lem  17238  qtopval  17313  isfbas  17451  fbssfi  17459  fsubbas  17489  fgval  17492  filssufil  17534  hauspwpwf1  17609  hauspwpwdom  17610  flimfnfcls  17650  ptcmplem1  17673  tsmsfbas  17737  eltsms  17742  blfval  17874  issubgo  20895  iscvm  23127  cvmsval  23134  altxpexg  23852  hfpw  24155  iscst1  24506  qusp  24874  efilcp  24884  islimrs  24912  lemindclsbu  25327  islocfin  25628  neibastop2lem  25641  fnemeet2  25648  fnejoin1  25649  elrfi  26101  elrfirn  26102  kelac2  26495
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-pow 4126
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108  df-pw 3568
  Copyright terms: Public domain W3C validator