Theorem pwexd 5318

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pow 5304

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544

This theorem is referenced by:  fabexd  7883  undefval  8221  mapexOLD  8774  pmvalg  8779  fopwdom  9018  pwdom  9062  fineqvlem  9171  fival  9320  fipwuni  9334  hartogslem2  9453  wdompwdom  9488  harwdom  9501  canthwe  10569  canthp1lem2  10571  gchdjuidm  10586  gchpwdom  10588  gchhar  10597  prdsmulr  17417  selvffval  22113  toponsspwpw  22901  mretopd  23071  ordtbaslem  23167  ptcmplem1  24031  isust  24183  blfvalps  24362  esplympl  33730  carsgval  34467  neibastop2lem  36562  bj-imdirvallem  37514  bj-imdirval2lem  37516  rfovcnvf1od  44453  fsovfd  44461  fsovcnvlem  44462  dssmapnvod  44469  dssmapf1od  44470  ntrneif1o  44524  ntrneicnv  44527  ntrneiel  44530  clsneiel1  44557  neicvgf1o  44563  neicvgnvo  44564  neicvgel1  44568  ntrelmap  44574  clselmap  44576  salexct  46784  psmeasurelem  46920  caragenval  46943  omeunile  46955  0ome  46979  isomennd  46981  afv2ex  47678  gpgvtx  48535  gpgiedg  48536