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

Theorem pwexg 4636
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 4015 . . 3
21eleq1d 2526 . 2
3 vex 3112 . . 3
43pwex 4635 . 2
52, 4vtoclg 3167 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818   cvv 3109  ~Pcpw 4012
This theorem is referenced by:  abssexg  4637  snexALT  4638  pwel  4704  xpexg  6602  uniexb  6610  fabexg  6756  undefval  7024  mapex  7445  pmvalg  7450  pw2eng  7643  fopwdom  7645  pwdom  7689  2pwne  7693  disjen  7694  domss2  7696  ssenen  7711  fineqvlem  7754  fival  7892  fipwuni  7906  hartogslem2  7989  wdompwdom  8025  harwdom  8037  tskwe  8352  ween  8437  acni  8447  acnnum  8454  infpwfien  8464  pwcda1  8595  ackbij1b  8640  fictb  8646  fin2i  8696  isfin2-2  8720  ssfin3ds  8731  fin23lem32  8745  fin23lem39  8751  fin23lem41  8753  isfin1-3  8787  fin1a2lem12  8812  canth3  8957  ondomon  8959  canthnum  9048  canthwe  9050  canthp1lem2  9052  gchxpidm  9068  gchpwdom  9069  gchhar  9078  wrdexg  12557  hashbcval  14520  restid2  14828  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  ismre  14987  isacs1i  15054  sscpwex  15184  fpwipodrs  15794  acsdrscl  15800  sylow2a  16639  opsrval  18139  istps3OLD  19423  tgdom  19480  distop  19497  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  cldval  19524  ntrfval  19525  clsfval  19526  mretopd  19593  neifval  19600  neif  19601  neival  19603  neiptoptop  19632  lpfval  19639  restfpw  19680  ordtbaslem  19689  islocfin  20018  dissnref  20029  kgenval  20036  dfac14lem  20118  qtopval  20196  isfbas  20330  fbssfi  20338  fsubbas  20368  fgval  20371  filssufil  20413  hauspwpwf1  20488  hauspwpwdom  20489  flimfnfcls  20529  ptcmplem1  20552  tsmsfbas  20626  eltsms  20631  ustval  20705  isust  20706  utopval  20735  blfvalps  20886  cusgraexilem1  24466  issubgo  25305  indv  28026  sigaex  28109  sigaval  28110  pwsiga  28130  omsval  28264  omsfval  28265  coinflipspace  28419  iscvm  28704  cvmsval  28711  altxpexg  29628  hfpw  29842  neibastop2lem  30178  fnemeet2  30185  fnejoin1  30186  elrfi  30626  elrfirn  30627  kelac2  31011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-pow 4630
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014
  Copyright terms: Public domain W3C validator