Theorem pwexg 4880

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 4194	. . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
2	1	eleq1d 2715	. 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3		vpwex 4879	. 2 ⊢ 𝒫 𝑥 ∈ V
4	2, 3	vtoclg 3297	1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030  Vcvv 3231  𝒫 cpw 4191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-pow 4873

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193

This theorem is referenced by:  abssexg  4881  snexALT  4882  pwel  4950  xpexg  7002  uniexr  7014  pwexb  7017  fabexg  7164  undefval  7447  mapex  7905  pmvalg  7910  pw2eng  8107  fopwdom  8109  pwdom  8153  2pwne  8157  disjen  8158  domss2  8160  ssenen  8175  fineqvlem  8215  fival  8359  fipwuni  8373  hartogslem2  8489  wdompwdom  8524  harwdom  8536  tskwe  8814  ween  8896  acni  8906  acnnum  8913  infpwfien  8923  pwcda1  9054  ackbij1b  9099  fictb  9105  fin2i  9155  isfin2-2  9179  ssfin3ds  9190  fin23lem32  9204  fin23lem39  9210  fin23lem41  9212  isfin1-3  9246  fin1a2lem12  9271  canth3  9421  ondomon  9423  canthnum  9509  canthwe  9511  canthp1lem2  9513  gchxpidm  9529  gchpwdom  9530  gchhar  9539  wrdexg  13347  hashbcval  15753  restid2  16138  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  ismre  16297  isacs1i  16365  sscpwex  16522  fpwipodrs  17211  acsdrscl  17217  sylow2a  18080  opsrval  19522  toponsspwpw  20774  tgdom  20830  distop  20847  fctop  20856  cctop  20858  ppttop  20859  epttop  20861  cldval  20875  ntrfval  20876  clsfval  20877  mretopd  20944  neifval  20951  neif  20952  neival  20954  neiptoptop  20983  lpfval  20990  restfpw  21031  ordtbaslem  21040  islocfin  21368  dissnref  21379  kgenval  21386  dfac14lem  21468  qtopval  21546  isfbas  21680  fbssfi  21688  fsubbas  21718  fgval  21721  filssufil  21763  hauspwpwf1  21838  hauspwpwdom  21839  flimfnfcls  21879  ptcmplem1  21903  tsmsfbas  21978  eltsms  21983  ustval  22053  isust  22054  utopval  22083  blfvalps  22235  cusgrexilem1  26391  indv  30202  sigaex  30300  sigaval  30301  pwsiga  30321  pwldsys  30348  ldgenpisyslem1  30354  omsval  30483  carsgval  30493  coinflipspace  30670  iscvm  31367  cvmsval  31374  madeval  32060  altxpexg  32210  hfpw  32417  neibastop2lem  32480  fnemeet2  32487  fnejoin1  32488  bj-restpw  33170  bj-discrmoore  33191  elrfi  37574  elrfirn  37575  kelac2  37952  enmappwid  38611  rfovd  38612  rfovcnvf1od  38615  fsovrfovd  38620  fsovfd  38623  fsovcnvlem  38624  dssmapfv2d  38629  dssmapnvod  38631  dssmapf1od  38632  clsk3nimkb  38655  ntrneif1o  38690  ntrneicnv  38693  ntrneiel  38696  clsneif1o  38719  clsneicnv  38720  clsneikex  38721  clsneinex  38722  clsneiel1  38723  neicvgf1o  38729  neicvgnvo  38730  neicvgmex  38732  neicvgel1  38734  ntrelmap  38740  clselmap  38742  pwexd  39596  pwsal  40853  salexct  40870  psmeasurelem  41005  caragenval  41028  omeunile  41040  0ome  41064  isomennd  41066