Theorem pwexd 5302

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3432  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-pow 5288

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  undefval  8092  mapex  8621  pmvalg  8626  fopwdom  8867  pwdom  8916  fineqvlem  9037  fival  9171  fipwuni  9185  hartogslem2  9302  wdompwdom  9337  harwdom  9350  canthwe  10407  canthp1lem2  10409  gchdjuidm  10424  gchpwdom  10426  gchhar  10435  prdsmulr  17170  selvffval  21326  toponsspwpw  22071  mretopd  22243  ordtbaslem  22339  ptcmplem1  23203  isust  23355  blfvalps  23536  carsgval  32270  neibastop2lem  34549  bj-imdirvallem  35351  bj-imdirval2lem  35353  rfovcnvf1od  41612  fsovfd  41620  fsovcnvlem  41621  dssmapnvod  41628  dssmapf1od  41629  ntrneif1o  41685  ntrneicnv  41688  ntrneiel  41691  clsneiel1  41718  neicvgf1o  41724  neicvgnvo  41725  neicvgel1  41729  ntrelmap  41735  clselmap  41737  salexct  43873  psmeasurelem  44008  caragenval  44031  omeunile  44043  0ome  44067  isomennd  44069  afv2ex  44706