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

Theorem pwexg 5055
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 4361 . . 3 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
21eleq1d 2877 . 2 (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3 vpwex 5054 . 2 𝒫 𝑥 ∈ V
42, 3vtoclg 3466 1 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2157  Vcvv 3398  𝒫 cpw 4358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791  ax-sep 4982  ax-pow 5042
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-v 3400  df-in 3783  df-ss 3790  df-pw 4360
This theorem is referenced by:  pwexd  5056  pwex  5057  abssexg  5058  snexALT  5059  pwel  5117  xpexg  7193  uniexr  7205  pwexb  7208  fabexg  7355  pw2eng  8308  2pwne  8358  disjen  8359  domss2  8361  ssenen  8376  fineqvlem  8416  tskwe  9062  ween  9144  acni  9154  acnnum  9161  infpwfien  9171  pwcda1  9304  ackbij1lem5  9334  ackbij1b  9349  fictb  9355  fin2i  9405  isfin2-2  9429  ssfin3ds  9440  fin23lem32  9454  fin23lem39  9460  fin23lem41  9462  isfin1-3  9496  fin1a2lem12  9521  canth3  9671  ondomon  9673  canthnum  9759  canthwe  9761  gchxpidm  9779  hashbcval  15926  restid2  16299  prdsplusg  16326  prdsvsca  16328  ismre  16458  isacs1i  16525  sscpwex  16682  fpwipodrs  17372  acsdrscl  17378  opsrval  19686  toponsspwpw  20944  tgdom  21000  distop  21017  fctop  21026  cctop  21028  ppttop  21029  epttop  21031  cldval  21045  ntrfval  21046  clsfval  21047  neifval  21121  neif  21122  neival  21124  neiptoptop  21153  lpfval  21160  restfpw  21201  islocfin  21538  dissnref  21549  kgenval  21556  dfac14lem  21638  qtopval  21716  isfbas  21850  fbssfi  21858  fsubbas  21888  fgval  21891  filssufil  21933  hauspwpwf1  22008  hauspwpwdom  22009  flimfnfcls  22049  tsmsfbas  22148  eltsms  22153  ustval  22223  utopval  22253  cusgrexilem1  26569  indv  30405  sigaex  30503  sigaval  30504  pwsiga  30524  pwldsys  30551  ldgenpisyslem1  30557  omsval  30686  carsgval  30696  coinflipspace  30873  iscvm  31569  cvmsval  31576  madeval  32261  altxpexg  32411  hfpw  32618  fnemeet2  32688  fnejoin1  32689  bj-restpw  33358  bj-discrmoore  33379  elrfi  37760  elrfirn  37761  kelac2  38137  enmappwid  38795  rfovd  38796  fsovrfovd  38804  dssmapfv2d  38813  clsk3nimkb  38839  clsneif1o  38903  clsneicnv  38904  clsneikex  38905  clsneinex  38906  neicvgmex  38916  neicvgel1  38918  pwsal  41015
  Copyright terms: Public domain W3C validator