Theorem pwexd 5321

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429  𝒫 cpw 4541

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 2708  ax-sep 5231  ax-pow 5307

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543

This theorem is referenced by:  fabexd  7888  undefval  8226  mapexOLD  8779  pmvalg  8784  fopwdom  9023  pwdom  9067  fineqvlem  9176  fival  9325  fipwuni  9339  hartogslem2  9458  wdompwdom  9493  harwdom  9506  canthwe  10574  canthp1lem2  10576  gchdjuidm  10591  gchpwdom  10593  gchhar  10602  prdsmulr  17422  selvffval  22099  toponsspwpw  22887  mretopd  23057  ordtbaslem  23153  ptcmplem1  24017  isust  24169  blfvalps  24348  esplympl  33711  carsgval  34447  neibastop2lem  36542  bj-imdirvallem  37494  bj-imdirval2lem  37496  rfovcnvf1od  44431  fsovfd  44439  fsovcnvlem  44440  dssmapnvod  44447  dssmapf1od  44448  ntrneif1o  44502  ntrneicnv  44505  ntrneiel  44508  clsneiel1  44535  neicvgf1o  44541  neicvgnvo  44542  neicvgel1  44546  ntrelmap  44552  clselmap  44554  salexct  46762  psmeasurelem  46898  caragenval  46921  omeunile  46933  0ome  46957  isomennd  46959  afv2ex  47662  gpgvtx  48519  gpgiedg  48520