Theorem pwexg 5377

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.

Step	Hyp	Ref	Expression
1		pweq 4613	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2825	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5376	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3553	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  Vcvv 3479  𝒫 cpw 4599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-pow 5364

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-pw 4601

This theorem is referenced by:  pwexd  5378  pwex  5379  pwel  5380  abssexg  5381  snexALT  5382  xpexg  7771  uniexr  7784  pwexb  7787  fabexgOLD  7962  pw2eng  9119  2pwne  9174  disjen  9175  domss2  9177  ssenen  9192  fineqvlem  9299  tskwe  9991  ween  10076  acni  10086  acnnum  10093  infpwfien  10103  pwdju1  10232  ackbij1b  10279  fictb  10285  fin2i  10336  isfin2-2  10360  ssfin3ds  10371  fin23lem32  10385  fin23lem39  10391  fin23lem41  10393  isfin1-3  10427  fin1a2lem12  10452  canth3  10602  ondomon  10604  canthnum  10690  canthwe  10692  gchxpidm  10710  hashbcval  17041  restid2  17476  prdsplusg  17504  prdsvsca  17506  ismre  17634  isacs1i  17701  sscpwex  17860  fpwipodrs  18586  acsdrscl  18592  opsrval  22065  toponsspwpw  22929  tgdom  22986  distop  23003  fctop  23012  cctop  23014  ppttop  23015  epttop  23017  cldval  23032  ntrfval  23033  clsfval  23034  neifval  23108  neif  23109  neival  23111  neiptoptop  23140  lpfval  23147  restfpw  23188  islocfin  23526  dissnref  23537  kgenval  23544  dfac14lem  23626  qtopval  23704  isfbas  23838  fbssfi  23846  fsubbas  23876  fgval  23879  filssufil  23921  hauspwpwf1  23996  hauspwpwdom  23997  flimfnfcls  24037  tsmsfbas  24137  eltsms  24142  ustval  24212  utopval  24242  madeval  27892  cusgrexilem1  29457  indv  32838  pwrssmgc  32991  sigaex  34112  sigaval  34113  pwsiga  34132  pwldsys  34159  ldgenpisyslem1  34165  omsval  34296  carsgval  34306  coinflipspace  34484  iscvm  35265  cvmsval  35272  ex-sategoelel  35427  altxpexg  35980  hfpw  36187  fnemeet2  36369  fnejoin1  36370  bj-restpw  37094  elrfi  42710  elrfirn  42711  kelac2  43082  enmappwid  44018  rfovd  44019  fsovrfovd  44027  dssmapfv2d  44036  clsk3nimkb  44058  clsneif1o  44122  clsneicnv  44123  clsneikex  44124  clsneinex  44125  neicvgmex  44135  neicvgel1  44137  pwsal  46335  prproropen  47500  stgrvtx  47926  stgriedg  47927