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

Theorem pwexg 4776
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 (𝐴𝑉 → 𝒫 𝐴 ∈ V)

Proof of Theorem pwexg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 pweq 4111 . . 3 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
21eleq1d 2672 . 2 (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3 vpwex 4775 . 2 𝒫 𝑥 ∈ V
42, 3vtoclg 3239 1 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  Vcvv 3173  𝒫 cpw 4108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-pow 4769
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110
This theorem is referenced by:  abssexg  4777  snexALT  4778  pwel  4847  xpexg  6858  uniexb  6866  fabexg  7015  undefval  7289  mapex  7750  pmvalg  7755  pw2eng  7951  fopwdom  7953  pwdom  7997  2pwne  8001  disjen  8002  domss2  8004  ssenen  8019  fineqvlem  8059  fival  8201  fipwuni  8215  hartogslem2  8331  wdompwdom  8366  harwdom  8378  tskwe  8659  ween  8741  acni  8751  acnnum  8758  infpwfien  8768  pwcda1  8899  ackbij1b  8944  fictb  8950  fin2i  9000  isfin2-2  9024  ssfin3ds  9035  fin23lem32  9049  fin23lem39  9055  fin23lem41  9057  isfin1-3  9091  fin1a2lem12  9116  canth3  9262  ondomon  9264  canthnum  9350  canthwe  9352  canthp1lem2  9354  gchxpidm  9370  gchpwdom  9371  gchhar  9380  wrdexg  13170  hashbcval  15544  restid2  15914  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  ismre  16073  isacs1i  16141  sscpwex  16298  fpwipodrs  16987  acsdrscl  16993  sylow2a  17857  opsrval  19295  tgdom  20593  distop  20610  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  cldval  20637  ntrfval  20638  clsfval  20639  mretopd  20706  neifval  20713  neif  20714  neival  20716  neiptoptop  20745  lpfval  20752  restfpw  20793  ordtbaslem  20802  islocfin  21130  dissnref  21141  kgenval  21148  dfac14lem  21230  qtopval  21308  isfbas  21443  fbssfi  21451  fsubbas  21481  fgval  21484  filssufil  21526  hauspwpwf1  21601  hauspwpwdom  21602  flimfnfcls  21642  ptcmplem1  21666  tsmsfbas  21741  eltsms  21746  ustval  21816  isust  21817  utopval  21846  blfvalps  21998  cusgraexilem1  25995  indv  29402  sigaex  29499  sigaval  29500  pwsiga  29520  pwldsys  29547  ldgenpisyslem1  29553  omsval  29682  carsgval  29692  coinflipspace  29869  iscvm  30495  cvmsval  30502  altxpexg  31255  hfpw  31462  neibastop2lem  31525  fnemeet2  31532  fnejoin1  31533  bj-restpw  32226  bj-toponss  32241  elrfi  36275  elrfirn  36276  kelac2  36653  enmappwid  37314  rfovd  37315  rfovcnvf1od  37318  fsovrfovd  37323  fsovfd  37326  fsovcnvlem  37327  dssmapfv2d  37332  dssmapnvod  37334  dssmapf1od  37335  clsk3nimkb  37358  ntrneif1o  37393  ntrneicnv  37396  ntrneiel  37399  clsneif1o  37422  clsneicnv  37423  clsneikex  37424  clsneinex  37425  clsneiel1  37426  neicvgf1o  37432  neicvgnvo  37433  neicvgmex  37435  neicvgel1  37437  ntrelmap  37443  clselmap  37445  pwexd  38311  pwsal  39211  salexct  39228  psmeasurelem  39363  caragenval  39383  omeunile  39395  0ome  39419  isomennd  39421  usgrexi  40661
  Copyright terms: Public domain W3C validator