Theorem pwexd 5311

Description: Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
pwexd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
pwexd	⊢ (𝜑 → 𝒫 𝐴 ∈ V)

Proof of Theorem pwexd

Step	Hyp	Ref	Expression
1		pwexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		pwexg 5310	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433  𝒫 cpw 4532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pow 5297

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-pw 4534

This theorem is referenced by:  fabexd  7881  undefval  8220  mapexOLD  8773  pmvalg  8778  fopwdom  9017  pwdom  9061  fineqvlem  9170  fival  9319  fipwuni  9333  hartogslem2  9452  wdompwdom  9487  harwdom  9500  canthwe  10569  canthp1lem2  10571  gchdjuidm  10586  gchpwdom  10588  gchhar  10597  prdsmulr  17417  selvffval  22098  toponsspwpw  22909  mretopd  23079  ordtbaslem  23175  ptcmplem1  24039  isust  24191  blfvalps  24370  esplympl  33763  carsgval  34499  neibastop2lem  36603  bj-imdirvallem  37555  bj-imdirval2lem  37557  rfovcnvf1od  44463  fsovfd  44471  fsovcnvlem  44472  dssmapnvod  44479  dssmapf1od  44480  ntrneif1o  44534  ntrneicnv  44537  ntrneiel  44540  clsneiel1  44567  neicvgf1o  44573  neicvgnvo  44574  neicvgel1  44578  ntrelmap  44584  clselmap  44586  salexct  46791  psmeasurelem  46927  caragenval  46950  omeunile  46962  0ome  46986  isomennd  46988  afv2ex  47691  gpgvtx  48548  gpgiedg  48549