Theorem pwexd 5384

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-pow 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-pw 4606

This theorem is referenced by:  fabexd  7957  undefval  8299  mapexOLD  8870  pmvalg  8875  fopwdom  9118  pwdom  9167  fineqvlem  9295  fival  9449  fipwuni  9463  hartogslem2  9580  wdompwdom  9615  harwdom  9628  canthwe  10688  canthp1lem2  10690  gchdjuidm  10705  gchpwdom  10707  gchhar  10716  prdsmulr  17505  selvffval  22154  toponsspwpw  22943  mretopd  23115  ordtbaslem  23211  ptcmplem1  24075  isust  24227  blfvalps  24408  carsgval  34284  neibastop2lem  36342  bj-imdirvallem  37162  bj-imdirval2lem  37164  rfovcnvf1od  43993  fsovfd  44001  fsovcnvlem  44002  dssmapnvod  44009  dssmapf1od  44010  ntrneif1o  44064  ntrneicnv  44067  ntrneiel  44070  clsneiel1  44097  neicvgf1o  44103  neicvgnvo  44104  neicvgel1  44108  ntrelmap  44114  clselmap  44116  salexct  46289  psmeasurelem  46425  caragenval  46448  omeunile  46460  0ome  46484  isomennd  46486  afv2ex  47163  gpgvtx  47937  gpgiedg  47938