Theorem pwexd 5297

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-pow 5283

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  undefval  8063  mapex  8579  pmvalg  8584  fopwdom  8820  pwdom  8865  fineqvlem  8966  fival  9101  fipwuni  9115  hartogslem2  9232  wdompwdom  9267  harwdom  9280  canthwe  10338  canthp1lem2  10340  gchdjuidm  10355  gchpwdom  10357  gchhar  10366  prdsmulr  17087  selvffval  21236  toponsspwpw  21979  mretopd  22151  ordtbaslem  22247  ptcmplem1  23111  isust  23263  blfvalps  23444  carsgval  32170  neibastop2lem  34476  bj-imdirvallem  35278  bj-imdirval2lem  35280  rfovcnvf1od  41501  fsovfd  41509  fsovcnvlem  41510  dssmapnvod  41517  dssmapf1od  41518  ntrneif1o  41574  ntrneicnv  41577  ntrneiel  41580  clsneiel1  41607  neicvgf1o  41613  neicvgnvo  41614  neicvgel1  41618  ntrelmap  41624  clselmap  41626  salexct  43763  psmeasurelem  43898  caragenval  43921  omeunile  43933  0ome  43957  isomennd  43959  afv2ex  44593