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

Theorem pwexg 4448
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 3840 . . 3
21eleq1d 2488 . 2
3 vex 2954 . . 3
43pwex 4447 . 2
52, 4vtoclg 3008 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1687  e.wcel 1749   cvv 2951  ~Pcpw 3837
This theorem is referenced by:  abssexg  4449  snexALT  4450  pwel  4516  uniexb  6356  xpexg  6477  fabexg  6502  undefval  6754  mapex  7181  pmvalg  7186  pw2eng  7376  fopwdom  7378  pwdom  7422  2pwne  7426  disjen  7427  domss2  7429  ssenen  7444  fineqvlem  7486  fival  7609  fipwuni  7623  hartogslem2  7704  wdompwdom  7740  harwdom  7752  tskwe  8067  ween  8152  acni  8162  acnnum  8169  infpwfien  8179  pwcda1  8310  ackbij1b  8355  fictb  8361  fin2i  8411  isfin2-2  8435  ssfin3ds  8446  fin23lem32  8460  fin23lem39  8466  fin23lem41  8468  isfin1-3  8502  fin1a2lem12  8527  canth3  8672  ondomon  8674  canthnum  8762  canthwe  8764  canthp1lem2  8766  gchxpidm  8782  gchpwdom  8783  gchhar  8792  wrdexg  12185  hashbcval  14003  restid2  14309  prdsplusg  14336  prdsmulr  14337  prdsvsca  14338  ismre  14468  isacs1i  14535  sscpwex  14668  fpwipodrs  15274  acsdrscl  15280  sylow2a  16055  opsrval  17358  istps3OLD  18231  tgdom  18287  distop  18304  fctop  18312  cctop  18314  ppttop  18315  epttop  18317  cldval  18331  ntrfval  18332  clsfval  18333  mretopd  18400  neifval  18407  neif  18408  neival  18410  neiptoptop  18439  lpfval  18446  restfpw  18487  ordtbaslem  18496  kgenval  18812  dfac14lem  18894  qtopval  18972  isfbas  19106  fbssfi  19114  fsubbas  19144  fgval  19147  filssufil  19189  hauspwpwf1  19264  hauspwpwdom  19265  flimfnfcls  19305  ptcmplem1  19328  tsmsfbas  19402  eltsms  19407  ustval  19477  isust  19478  utopval  19507  blfvalps  19658  cusgraexilem1  23053  issubgo  23469  indv  26178  sigaex  26261  sigaval  26262  pwsiga  26282  coinflipspace  26566  iscvm  26851  cvmsval  26858  altxpexg  27711  hfpw  27925  islocfin  28239  neibastop2lem  28252  fnemeet2  28259  fnejoin1  28260  elrfi  28702  elrfirn  28703  kelac2  29091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-pow 4442
This theorem depends on definitions:  df-bi 179  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-v 2953  df-in 3312  df-ss 3319  df-pw 3839
  Copyright terms: Public domain W3C validator