Theorem pwexg 5323

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 4568	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2821	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5322	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3511	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pow 5310

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-pw 4556

This theorem is referenced by:  pwexd  5324  pwex  5325  pwel  5326  abssexg  5327  snexALT  5328  xpexg  7695  uniexr  7708  pwexb  7711  fabexgOLD  7881  pw2eng  9011  2pwne  9061  disjen  9062  domss2  9064  ssenen  9079  fineqvlem  9166  tskwe  9862  ween  9945  acni  9955  acnnum  9962  infpwfien  9972  pwdju1  10101  ackbij1b  10148  fictb  10154  fin2i  10205  isfin2-2  10229  ssfin3ds  10240  fin23lem32  10254  fin23lem39  10260  fin23lem41  10262  isfin1-3  10296  fin1a2lem12  10321  canth3  10471  ondomon  10473  canthnum  10560  canthwe  10562  gchxpidm  10580  hashbcval  16930  restid2  17350  prdsplusg  17378  prdsvsca  17380  ismre  17509  isacs1i  17580  sscpwex  17739  fpwipodrs  18463  acsdrscl  18469  opsrval  22001  toponsspwpw  22866  tgdom  22922  distop  22939  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  cldval  22967  ntrfval  22968  clsfval  22969  neifval  23043  neif  23044  neival  23046  neiptoptop  23075  lpfval  23082  restfpw  23123  islocfin  23461  dissnref  23472  kgenval  23479  dfac14lem  23561  qtopval  23639  isfbas  23773  fbssfi  23781  fsubbas  23811  fgval  23814  filssufil  23856  hauspwpwf1  23931  hauspwpwdom  23932  flimfnfcls  23972  tsmsfbas  24072  eltsms  24077  ustval  24147  utopval  24176  madeval  27828  cusgrexilem1  29512  indv  32931  pwrssmgc  33082  sigaex  34267  sigaval  34268  pwsiga  34287  pwldsys  34314  ldgenpisyslem1  34320  omsval  34450  carsgval  34460  coinflipspace  34638  iscvm  35453  cvmsval  35460  ex-sategoelel  35615  altxpexg  36172  hfpw  36379  fnemeet2  36561  fnejoin1  36562  bj-restpw  37293  elrfi  42932  elrfirn  42933  kelac2  43303  enmappwid  44237  rfovd  44238  fsovrfovd  44246  dssmapfv2d  44255  clsk3nimkb  44277  clsneif1o  44341  clsneicnv  44342  clsneikex  44343  clsneinex  44344  neicvgmex  44354  neicvgel1  44356  pwsal  46555  prproropen  47750  stgrvtx  48196  stgriedg  48197