Theorem pwexd 5315

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3434  𝒫 cpw 4548

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 2112  ax-9 2120  ax-ext 2702  ax-sep 5232  ax-pow 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-ss 3917  df-pw 4550

This theorem is referenced by:  fabexd  7862  undefval  8201  mapexOLD  8751  pmvalg  8756  fopwdom  8993  pwdom  9037  fineqvlem  9145  fival  9291  fipwuni  9305  hartogslem2  9424  wdompwdom  9459  harwdom  9472  canthwe  10534  canthp1lem2  10536  gchdjuidm  10551  gchpwdom  10553  gchhar  10562  prdsmulr  17355  selvffval  22041  toponsspwpw  22830  mretopd  23000  ordtbaslem  23096  ptcmplem1  23960  isust  24112  blfvalps  24291  esplympl  33578  carsgval  34306  neibastop2lem  36373  bj-imdirvallem  37193  bj-imdirval2lem  37195  rfovcnvf1od  44016  fsovfd  44024  fsovcnvlem  44025  dssmapnvod  44032  dssmapf1od  44033  ntrneif1o  44087  ntrneicnv  44090  ntrneiel  44093  clsneiel1  44120  neicvgf1o  44126  neicvgnvo  44127  neicvgel1  44131  ntrelmap  44137  clselmap  44139  salexct  46351  psmeasurelem  46487  caragenval  46510  omeunile  46522  0ome  46546  isomennd  46548  afv2ex  47224  gpgvtx  48053  gpgiedg  48054