Theorem pwexg 4850

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.

Step	Hyp	Ref	Expression
1		pweq 4161	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2686	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 4849	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3266	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  Vcvv 3200  𝒫 cpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-pow 4843

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  abssexg  4851  snexALT  4852  pwel  4920  xpexg  6960  uniexr  6972  pwexb  6975  fabexg  7122  undefval  7402  mapex  7863  pmvalg  7868  pw2eng  8066  fopwdom  8068  pwdom  8112  2pwne  8116  disjen  8117  domss2  8119  ssenen  8134  fineqvlem  8174  fival  8318  fipwuni  8332  hartogslem2  8448  wdompwdom  8483  harwdom  8495  tskwe  8776  ween  8858  acni  8868  acnnum  8875  infpwfien  8885  pwcda1  9016  ackbij1b  9061  fictb  9067  fin2i  9117  isfin2-2  9141  ssfin3ds  9152  fin23lem32  9166  fin23lem39  9172  fin23lem41  9174  isfin1-3  9208  fin1a2lem12  9233  canth3  9383  ondomon  9385  canthnum  9471  canthwe  9473  canthp1lem2  9475  gchxpidm  9491  gchpwdom  9492  gchhar  9501  wrdexg  13315  hashbcval  15706  restid2  16091  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  ismre  16250  isacs1i  16318  sscpwex  16475  fpwipodrs  17164  acsdrscl  17170  sylow2a  18034  opsrval  19474  toponsspwpw  20726  tgdom  20782  distop  20799  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  cldval  20827  ntrfval  20828  clsfval  20829  mretopd  20896  neifval  20903  neif  20904  neival  20906  neiptoptop  20935  lpfval  20942  restfpw  20983  ordtbaslem  20992  islocfin  21320  dissnref  21331  kgenval  21338  dfac14lem  21420  qtopval  21498  isfbas  21633  fbssfi  21641  fsubbas  21671  fgval  21674  filssufil  21716  hauspwpwf1  21791  hauspwpwdom  21792  flimfnfcls  21832  ptcmplem1  21856  tsmsfbas  21931  eltsms  21936  ustval  22006  isust  22007  utopval  22036  blfvalps  22188  cusgrexilem1  26335  indv  30074  sigaex  30172  sigaval  30173  pwsiga  30193  pwldsys  30220  ldgenpisyslem1  30226  omsval  30355  carsgval  30365  coinflipspace  30542  iscvm  31241  cvmsval  31248  madeval  31935  altxpexg  32085  hfpw  32292  neibastop2lem  32355  fnemeet2  32362  fnejoin1  32363  bj-restpw  33045  bj-discrmoore  33066  elrfi  37257  elrfirn  37258  kelac2  37635  enmappwid  38294  rfovd  38295  rfovcnvf1od  38298  fsovrfovd  38303  fsovfd  38306  fsovcnvlem  38307  dssmapfv2d  38312  dssmapnvod  38314  dssmapf1od  38315  clsk3nimkb  38338  ntrneif1o  38373  ntrneicnv  38376  ntrneiel  38379  clsneif1o  38402  clsneicnv  38403  clsneikex  38404  clsneinex  38405  clsneiel1  38406  neicvgf1o  38412  neicvgnvo  38413  neicvgmex  38415  neicvgel1  38417  ntrelmap  38423  clselmap  38425  pwexd  39282  pwsal  40535  salexct  40552  psmeasurelem  40687  caragenval  40707  omeunile  40719  0ome  40743  isomennd  40745