Theorem pwexd 5379

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480  𝒫 cpw 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pow 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-pw 4602

This theorem is referenced by:  fabexd  7959  undefval  8301  mapexOLD  8872  pmvalg  8877  fopwdom  9120  pwdom  9169  fineqvlem  9298  fival  9452  fipwuni  9466  hartogslem2  9583  wdompwdom  9618  harwdom  9631  canthwe  10691  canthp1lem2  10693  gchdjuidm  10708  gchpwdom  10710  gchhar  10719  prdsmulr  17504  selvffval  22137  toponsspwpw  22928  mretopd  23100  ordtbaslem  23196  ptcmplem1  24060  isust  24212  blfvalps  24393  carsgval  34305  neibastop2lem  36361  bj-imdirvallem  37181  bj-imdirval2lem  37183  rfovcnvf1od  44017  fsovfd  44025  fsovcnvlem  44026  dssmapnvod  44033  dssmapf1od  44034  ntrneif1o  44088  ntrneicnv  44091  ntrneiel  44094  clsneiel1  44121  neicvgf1o  44127  neicvgnvo  44128  neicvgel1  44132  ntrelmap  44138  clselmap  44140  salexct  46349  psmeasurelem  46485  caragenval  46508  omeunile  46520  0ome  46544  isomennd  46546  afv2ex  47226  gpgvtx  48002  gpgiedg  48003