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

Theorem pwexg 5267
Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (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 4539 . . 3 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
21eleq1d 2900 . 2 (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3 vpwex 5266 . 2 𝒫 𝑥 ∈ V
42, 3vtoclg 3554 1 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  Vcvv 3481  𝒫 cpw 4523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-pow 5254
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3483  df-in 3927  df-ss 3937  df-pw 4525
This theorem is referenced by:  pwexd  5268  pwex  5269  pwel  5270  abssexg  5271  snexALT  5272  xpexg  7468  uniexr  7480  pwexb  7483  fabexg  7635  pw2eng  8620  2pwne  8671  disjen  8672  domss2  8674  ssenen  8689  fineqvlem  8730  tskwe  9377  ween  9460  acni  9470  acnnum  9477  infpwfien  9487  pwdju1  9615  ackbij1b  9660  fictb  9666  fin2i  9716  isfin2-2  9740  ssfin3ds  9751  fin23lem32  9765  fin23lem39  9771  fin23lem41  9773  isfin1-3  9807  fin1a2lem12  9832  canth3  9982  ondomon  9984  canthnum  10070  canthwe  10072  gchxpidm  10090  hashbcval  16339  restid2  16707  prdsplusg  16734  prdsvsca  16736  ismre  16864  isacs1i  16931  sscpwex  17088  fpwipodrs  17777  acsdrscl  17783  opsrval  20258  toponsspwpw  21533  tgdom  21589  distop  21606  fctop  21615  cctop  21617  ppttop  21618  epttop  21620  cldval  21634  ntrfval  21635  clsfval  21636  neifval  21710  neif  21711  neival  21713  neiptoptop  21742  lpfval  21749  restfpw  21790  islocfin  22128  dissnref  22139  kgenval  22146  dfac14lem  22228  qtopval  22306  isfbas  22440  fbssfi  22448  fsubbas  22478  fgval  22481  filssufil  22523  hauspwpwf1  22598  hauspwpwdom  22599  flimfnfcls  22639  tsmsfbas  22739  eltsms  22744  ustval  22814  utopval  22844  cusgrexilem1  27235  pwrssmgc  30694  indv  31331  sigaex  31429  sigaval  31430  pwsiga  31449  pwldsys  31476  ldgenpisyslem1  31482  omsval  31611  carsgval  31621  coinflipspace  31798  iscvm  32566  cvmsval  32573  ex-sategoelel  32728  madeval  33349  altxpexg  33499  hfpw  33706  fnemeet2  33775  fnejoin1  33776  bj-restpw  34454  elrfi  39552  elrfirn  39553  kelac2  39926  enmappwid  40619  rfovd  40620  fsovrfovd  40628  dssmapfv2d  40637  clsk3nimkb  40663  clsneif1o  40727  clsneicnv  40728  clsneikex  40729  clsneinex  40730  neicvgmex  40740  neicvgel1  40742  pwsal  42884  prproropen  43952
  Copyright terms: Public domain W3C validator