Theorem pwexg 5334

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 2846	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5333	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3521	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  Vcvv 3453  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pow 5321

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-pw 4556

This theorem is referenced by:  pwexd  5335  pwex  5336  pwel  5337  abssexg  5338  snexALT  5339  xpexg  7729  uniexr  7742  pwexb  7745  pw2eng  9051  2pwne  9101  disjen  9102  domss2  9104  ssenen  9119  fineqvlem  9206  tskwe  9905  ween  9988  acni  9998  acnnum  10005  infpwfien  10015  pwdju1  10144  ackbij1b  10191  fictb  10197  fin2i  10249  isfin2-2  10273  ssfin3ds  10284  fin23lem32  10298  fin23lem39  10304  fin23lem41  10306  isfin1-3  10340  fin1a2lem12  10365  canth3  10515  ondomon  10517  canthnum  10604  canthwe  10606  gchxpidm  10624  indv  12194  hashbcval  17021  restid2  17442  prdsplusg  17470  prdsvsca  17472  ismre  17601  isacs1i  17672  sscpwex  17831  fpwipodrs  18555  acsdrscl  18561  opsrval  22079  toponsspwpw  22962  tgdom  23018  distop  23035  fctop  23044  cctop  23046  ppttop  23047  epttop  23049  cldval  23063  ntrfval  23064  clsfval  23065  neifval  23139  neif  23140  neival  23142  neiptoptop  23171  lpfval  23178  restfpw  23219  islocfin  23557  dissnref  23568  kgenval  23575  dfac14lem  23657  qtopval  23735  isfbas  23869  fbssfi  23877  fsubbas  23907  fgval  23910  filssufil  23952  hauspwpwf1  24027  hauspwpwdom  24028  flimfnfcls  24068  tsmsfbas  24168  eltsms  24173  ustval  24243  utopval  24272  madeval  27902  cusgrexilem1  29586  pwrssmgc  33139  sigaex  34368  sigaval  34369  pwsiga  34388  pwldsys  34415  ldgenpisyslem1  34421  omsval  34551  carsgval  34561  coinflipspace  34739  iscvm  35573  cvmsval  35580  ex-sategoelel  35735  altxpexg  36292  hfpw  36499  fnemeet2  36691  fnejoin1  36692  bj-restpw  37546  elrfi  43239  elrfirn  43240  kelac2  43606  enmappwid  44540  rfovd  44541  fsovrfovd  44549  dssmapfv2d  44558  clsk3nimkb  44580  clsneif1o  44644  clsneicnv  44645  clsneikex  44646  clsneinex  44647  neicvgmex  44657  neicvgel1  44659  pwsal  46853  prproropen  48078  stgrvtx  48540  stgriedg  48541