Theorem pwexd 5328

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 5327	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝒫 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pow 5314

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-pw 4558

This theorem is referenced by:  fabexd  7891  undefval  8230  mapexOLD  8783  pmvalg  8788  fopwdom  9027  pwdom  9071  fineqvlem  9180  fival  9329  fipwuni  9343  hartogslem2  9462  wdompwdom  9497  harwdom  9510  canthwe  10576  canthp1lem2  10578  gchdjuidm  10593  gchpwdom  10595  gchhar  10604  prdsmulr  17393  selvffval  22093  toponsspwpw  22883  mretopd  23053  ordtbaslem  23149  ptcmplem1  24013  isust  24165  blfvalps  24344  esplympl  33750  carsgval  34487  neibastop2lem  36582  bj-imdirvallem  37462  bj-imdirval2lem  37464  rfovcnvf1od  44389  fsovfd  44397  fsovcnvlem  44398  dssmapnvod  44405  dssmapf1od  44406  ntrneif1o  44460  ntrneicnv  44463  ntrneiel  44466  clsneiel1  44493  neicvgf1o  44499  neicvgnvo  44500  neicvgel1  44504  ntrelmap  44510  clselmap  44512  salexct  46721  psmeasurelem  46857  caragenval  46880  omeunile  46892  0ome  46916  isomennd  46918  afv2ex  47603  gpgvtx  48432  gpgiedg  48433