Theorem pwexd 5322

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438  𝒫 cpw 4552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-pow 5308

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-pw 4554

This theorem is referenced by:  fabexd  7877  undefval  8216  mapexOLD  8767  pmvalg  8772  fopwdom  9011  pwdom  9055  fineqvlem  9164  fival  9313  fipwuni  9327  hartogslem2  9446  wdompwdom  9481  harwdom  9494  canthwe  10560  canthp1lem2  10562  gchdjuidm  10577  gchpwdom  10579  gchhar  10588  prdsmulr  17377  selvffval  22074  toponsspwpw  22864  mretopd  23034  ordtbaslem  23130  ptcmplem1  23994  isust  24146  blfvalps  24325  esplympl  33674  carsgval  34409  neibastop2lem  36503  bj-imdirvallem  37324  bj-imdirval2lem  37326  rfovcnvf1od  44187  fsovfd  44195  fsovcnvlem  44196  dssmapnvod  44203  dssmapf1od  44204  ntrneif1o  44258  ntrneicnv  44261  ntrneiel  44264  clsneiel1  44291  neicvgf1o  44297  neicvgnvo  44298  neicvgel1  44302  ntrelmap  44308  clselmap  44310  salexct  46520  psmeasurelem  46656  caragenval  46679  omeunile  46691  0ome  46715  isomennd  46717  afv2ex  47402  gpgvtx  48231  gpgiedg  48232