Theorem pwexg 4771

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 4111	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2672	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 4770	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3239	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

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 4704  ax-pow 4764

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  4772  snexALT  4773  pwel  4841  xpexg  6836  uniexb  6844  fabexg  6993  undefval  7267  mapex  7728  pmvalg  7733  pw2eng  7929  fopwdom  7931  pwdom  7975  2pwne  7979  disjen  7980  domss2  7982  ssenen  7997  fineqvlem  8037  fival  8179  fipwuni  8193  hartogslem2  8309  wdompwdom  8344  harwdom  8356  tskwe  8637  ween  8719  acni  8729  acnnum  8736  infpwfien  8746  pwcda1  8877  ackbij1b  8922  fictb  8928  fin2i  8978  isfin2-2  9002  ssfin3ds  9013  fin23lem32  9027  fin23lem39  9033  fin23lem41  9035  isfin1-3  9069  fin1a2lem12  9094  canth3  9240  ondomon  9242  canthnum  9328  canthwe  9330  canthp1lem2  9332  gchxpidm  9348  gchpwdom  9349  gchhar  9358  wrdexg  13119  hashbcval  15493  restid2  15863  prdsplusg  15890  prdsmulr  15891  prdsvsca  15892  ismre  16022  isacs1i  16090  sscpwex  16247  fpwipodrs  16936  acsdrscl  16942  sylow2a  17806  opsrval  19244  tgdom  20541  distop  20558  fctop  20566  cctop  20568  ppttop  20569  epttop  20571  cldval  20585  ntrfval  20586  clsfval  20587  mretopd  20654  neifval  20661  neif  20662  neival  20664  neiptoptop  20693  lpfval  20700  restfpw  20741  ordtbaslem  20750  islocfin  21078  dissnref  21089  kgenval  21096  dfac14lem  21178  qtopval  21256  isfbas  21391  fbssfi  21399  fsubbas  21429  fgval  21432  filssufil  21474  hauspwpwf1  21549  hauspwpwdom  21550  flimfnfcls  21590  ptcmplem1  21614  tsmsfbas  21689  eltsms  21694  ustval  21764  isust  21765  utopval  21794  blfvalps  21946  cusgraexilem1  25789  indv  29196  sigaex  29293  sigaval  29294  pwsiga  29314  pwldsys  29341  ldgenpisyslem1  29347  omsval  29476  carsgval  29486  coinflipspace  29663  iscvm  30289  cvmsval  30296  altxpexg  31049  hfpw  31256  neibastop2lem  31319  fnemeet2  31326  fnejoin1  31327  bj-restpw  32020  bj-toponss  32035  elrfi  36069  elrfirn  36070  kelac2  36447  enmappwid  37108  rfovd  37109  rfovcnvf1od  37112  fsovrfovd  37117  fsovfd  37120  fsovcnvlem  37121  dssmapfv2d  37126  dssmapnvod  37128  dssmapf1od  37129  clsk3nimkb  37152  ntrneif1o  37187  ntrneicnv  37190  ntrneiel  37193  clsneif1o  37216  clsneicnv  37217  clsneikex  37218  clsneinex  37219  clsneiel1  37220  neicvgf1o  37226  neicvgnvo  37227  neicvgmex  37229  neicvgel1  37231  ntrelmap  37237  clselmap  37239  pwexd  38105  pwsal  39005  salexct  39022  psmeasurelem  39157  caragenval  39177  omeunile  39189  0ome  39213  isomennd  39215  usgrexi  40653