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

Theorem pwexg 4088
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 3533 . . 3  |-  ( x  =  A  ->  ~P x  =  ~P A
)
21eleq1d 2319 . 2  |-  ( x  =  A  ->  ( ~P x  e.  _V  <->  ~P A  e.  _V )
)
3 vex 2730 . . 3  |-  x  e. 
_V
43pwex 4087 . 2  |-  ~P x  e.  _V
52, 4vtoclg 2781 1  |-  ( A  e.  V  ->  ~P A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   _Vcvv 2727   ~Pcpw 3530
This theorem is referenced by:  abssexg  4089  snexALT  4090  pwel  4119  uniexb  4454  xpexg  4707  fabexg  5279  undefval  6187  mapex  6664  pmvalg  6669  pw2eng  6853  fopwdom  6855  pwdom  6898  2pwne  6902  disjen  6903  domss2  6905  ssenen  6920  fineqvlem  6962  fival  7050  fipwuni  7063  hartogslem2  7142  wdompwdom  7176  harwdom  7188  tskwe  7467  ween  7546  acni  7556  acnnum  7563  infpwfien  7573  pwcda1  7704  ackbij1b  7749  fictb  7755  fin2i  7805  isfin2-2  7829  ssfin3ds  7840  fin23lem32  7854  fin23lem39  7860  fin23lem41  7862  isfin1-3  7896  fin1a2lem12  7921  canth3  8065  ondomon  8067  canthnum  8151  canthwe  8153  canthp1lem2  8155  gchxpidm  8171  gchhar  8173  gchpwdom  8176  wrdexg  11302  hashbcval  12923  restid2  13209  prdsplusg  13232  prdsmulr  13233  prdsvsca  13234  ismre  13364  isacs1i  13403  sscpwex  13536  fpwipodrs  14111  acsdrscl  14117  sylow2a  14765  opsrval  16048  istps3OLD  16492  tgdom  16548  distop  16565  fctop  16573  cctop  16575  ppttop  16576  epttop  16578  cldval  16592  ntrfval  16593  clsfval  16594  mretopd  16661  neifval  16668  neif  16669  neival  16671  lpfval  16702  restfpw  16742  ordtbaslem  16750  kgenval  17062  dfac14lem  17143  qtopval  17218  isfbas  17356  fbssfi  17364  fsubbas  17394  fgval  17397  filssufil  17439  hauspwpwf1  17514  hauspwpwdom  17515  flimfnfcls  17555  ptcmplem1  17578  tsmsfbas  17642  eltsms  17647  blfval  17779  issubgo  20800  iscvm  22961  cvmsval  22968  altxpexg  23686  hfpw  23989  iscst1  24340  qusp  24708  efilcp  24718  islimrs  24746  lemindclsbu  25161  islocfin  25462  neibastop2lem  25475  fnemeet2  25482  fnejoin1  25483  elrfi  25935  elrfirn  25936  kelac2  26329
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 1926  ax-ext 2234  ax-sep 4038  ax-pow 4082
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-pw 3532
  Copyright terms: Public domain W3C validator