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

Theorem pwexg 4593
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

Proof of Theorem pwexg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 pweq 3979 . . 3
21eleq1d 2523 . 2
3 vex 3084 . . 3
43pwex 4592 . 2
52, 4vtoclg 3139 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1370  e.wcel 1758   cvv 3081  ~Pcpw 3976
This theorem is referenced by:  abssexg  4594  snexALT  4595  pwel  4661  uniexb  6519  xpexg  6640  fabexg  6666  undefval  6929  mapex  7354  pmvalg  7359  pw2eng  7551  fopwdom  7553  pwdom  7597  2pwne  7601  disjen  7602  domss2  7604  ssenen  7619  fineqvlem  7662  fival  7798  fipwuni  7812  hartogslem2  7894  wdompwdom  7930  harwdom  7942  tskwe  8257  ween  8342  acni  8352  acnnum  8359  infpwfien  8369  pwcda1  8500  ackbij1b  8545  fictb  8551  fin2i  8601  isfin2-2  8625  ssfin3ds  8636  fin23lem32  8650  fin23lem39  8656  fin23lem41  8658  isfin1-3  8692  fin1a2lem12  8717  canth3  8862  ondomon  8864  canthnum  8953  canthwe  8955  canthp1lem2  8957  gchxpidm  8973  gchpwdom  8974  gchhar  8983  wrdexg  12402  hashbcval  14221  restid2  14528  prdsplusg  14555  prdsmulr  14556  prdsvsca  14557  ismre  14687  isacs1i  14754  sscpwex  14887  fpwipodrs  15493  acsdrscl  15499  sylow2a  16279  opsrval  17733  istps3OLD  18926  tgdom  18982  distop  18999  fctop  19007  cctop  19009  ppttop  19010  epttop  19012  cldval  19026  ntrfval  19027  clsfval  19028  mretopd  19095  neifval  19102  neif  19103  neival  19105  neiptoptop  19134  lpfval  19141  restfpw  19182  ordtbaslem  19191  kgenval  19507  dfac14lem  19589  qtopval  19667  isfbas  19801  fbssfi  19809  fsubbas  19839  fgval  19842  filssufil  19884  hauspwpwf1  19959  hauspwpwdom  19960  flimfnfcls  20000  ptcmplem1  20023  tsmsfbas  20097  eltsms  20102  ustval  20176  isust  20177  utopval  20206  blfvalps  20357  cusgraexilem1  23843  issubgo  24259  indv  26926  sigaex  27009  sigaval  27010  pwsiga  27030  omsval  27164  omsfval  27165  coinflipspace  27319  iscvm  27604  cvmsval  27611  altxpexg  28465  hfpw  28679  islocfin  29028  neibastop2lem  29041  fnemeet2  29048  fnejoin1  29049  elrfi  29490  elrfirn  29491  kelac2  29878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-pow 4587
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3083  df-in 3449  df-ss 3456  df-pw 3978
  Copyright terms: Public domain W3C validator