Theorem pwexd 5338

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

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456  𝒫 cpw 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pow 5324

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-pw 4559

This theorem is referenced by:  fabexd  7920  undefval  8259  pmvalg  8820  fopwdom  9059  pwdom  9103  fineqvlem  9212  fival  9360  fipwuni  9374  hartogslem2  9493  wdompwdom  9528  harwdom  9541  canthwe  10611  canthp1lem2  10613  gchdjuidm  10628  gchpwdom  10630  gchhar  10639  prdsmulr  17490  selvffval  22173  toponsspwpw  22984  mretopd  23154  ordtbaslem  23250  ptcmplem1  24114  isust  24266  blfvalps  24445  esplympl  33866  carsgval  34602  neibastop2lem  36725  bj-imdirvallem  37677  bj-imdirval2lem  37679  rfovcnvf1od  44585  fsovfd  44593  fsovcnvlem  44594  dssmapnvod  44601  dssmapf1od  44602  ntrneif1o  44656  ntrneicnv  44659  ntrneiel  44662  clsneiel1  44689  neicvgf1o  44695  neicvgnvo  44696  neicvgel1  44700  ntrelmap  44706  clselmap  44708  salexct  46913  psmeasurelem  47049  caragenval  47072  omeunile  47084  0ome  47108  isomennd  47110  afv2ex  47813  gpgvtx  48670  gpgiedg  48671