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

Theorem pwexg 4166
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 3602 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2324 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2766 . . 3  |-  x  e. 
_V
43pwex 4165 . 2  |-  ~P x  e.  _V
52, 4vtoclg 2818 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   _Vcvv 2763   ~Pcpw 3599
This theorem is referenced by:  abssexg  4167  snexALT  4168  pwel  4197  uniexb  4535  xpexg  4788  fabexg  5360  undefval  6269  mapex  6746  pmvalg  6751  pw2eng  6936  fopwdom  6938  pwdom  6981  2pwne  6985  disjen  6986  domss2  6988  ssenen  7003  fineqvlem  7045  fival  7134  fipwuni  7147  hartogslem2  7226  wdompwdom  7260  harwdom  7272  tskwe  7551  ween  7630  acni  7640  acnnum  7647  infpwfien  7657  pwcda1  7788  ackbij1b  7833  fictb  7839  fin2i  7889  isfin2-2  7913  ssfin3ds  7924  fin23lem32  7938  fin23lem39  7944  fin23lem41  7946  isfin1-3  7980  fin1a2lem12  8005  canth3  8151  ondomon  8153  canthnum  8239  canthwe  8241  canthp1lem2  8243  gchxpidm  8259  gchhar  8261  gchpwdom  8264  wrdexg  11391  hashbcval  13012  restid2  13298  prdsplusg  13321  prdsmulr  13322  prdsvsca  13323  ismre  13455  isacs1i  13522  sscpwex  13655  fpwipodrs  14230  acsdrscl  14236  sylow2a  14893  opsrval  16179  istps3OLD  16623  tgdom  16679  distop  16696  fctop  16704  cctop  16706  ppttop  16707  epttop  16709  cldval  16723  ntrfval  16724  clsfval  16725  mretopd  16792  neifval  16799  neif  16800  neival  16802  lpfval  16833  restfpw  16873  ordtbaslem  16881  kgenval  17193  dfac14lem  17274  qtopval  17349  isfbas  17487  fbssfi  17495  fsubbas  17525  fgval  17528  filssufil  17570  hauspwpwf1  17645  hauspwpwdom  17646  flimfnfcls  17686  ptcmplem1  17709  tsmsfbas  17773  eltsms  17778  blfval  17910  issubgo  20931  iscvm  23163  cvmsval  23170  altxpexg  23888  hfpw  24191  iscst1  24542  qusp  24910  efilcp  24920  islimrs  24948  lemindclsbu  25363  islocfin  25664  neibastop2lem  25677  fnemeet2  25684  fnejoin1  25685  elrfi  26137  elrfirn  26138  kelac2  26531
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 2239  ax-sep 4115  ax-pow 4160
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-pw 3601
  Copyright terms: Public domain W3C validator