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 4617	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2816	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 5376	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3541	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  Vcvv 3472  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-pow 5364

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  pwexd  5378  pwex  5379  pwel  5380  abssexg  5381  snexALT  5382  xpexg  7741  uniexr  7754  pwexb  7757  fabexg  7929  pw2eng  9082  2pwne  9137  disjen  9138  domss2  9140  ssenen  9155  fineqvlem  9266  tskwe  9949  ween  10034  acni  10044  acnnum  10051  infpwfien  10061  pwdju1  10189  ackbij1b  10238  fictb  10244  fin2i  10294  isfin2-2  10318  ssfin3ds  10329  fin23lem32  10343  fin23lem39  10349  fin23lem41  10351  isfin1-3  10385  fin1a2lem12  10410  canth3  10560  ondomon  10562  canthnum  10648  canthwe  10650  gchxpidm  10668  hashbcval  16941  restid2  17382  prdsplusg  17410  prdsvsca  17412  ismre  17540  isacs1i  17607  sscpwex  17768  fpwipodrs  18499  acsdrscl  18505  opsrval  21822  toponsspwpw  22646  tgdom  22703  distop  22720  fctop  22729  cctop  22731  ppttop  22732  epttop  22734  cldval  22749  ntrfval  22750  clsfval  22751  neifval  22825  neif  22826  neival  22828  neiptoptop  22857  lpfval  22864  restfpw  22905  islocfin  23243  dissnref  23254  kgenval  23261  dfac14lem  23343  qtopval  23421  isfbas  23555  fbssfi  23563  fsubbas  23593  fgval  23596  filssufil  23638  hauspwpwf1  23713  hauspwpwdom  23714  flimfnfcls  23754  tsmsfbas  23854  eltsms  23859  ustval  23929  utopval  23959  madeval  27582  cusgrexilem1  28961  pwrssmgc  32435  indv  33306  sigaex  33404  sigaval  33405  pwsiga  33424  pwldsys  33451  ldgenpisyslem1  33457  omsval  33588  carsgval  33598  coinflipspace  33775  iscvm  34546  cvmsval  34553  ex-sategoelel  34708  altxpexg  35252  hfpw  35459  fnemeet2  35557  fnejoin1  35558  bj-restpw  36278  elrfi  41736  elrfirn  41737  kelac2  42111  enmappwid  43055  rfovd  43056  fsovrfovd  43064  dssmapfv2d  43073  clsk3nimkb  43095  clsneif1o  43159  clsneicnv  43160  clsneikex  43161  clsneinex  43162  neicvgmex  43172  neicvgel1  43174  pwsal  45331  prproropen  46476