Theorem pwexd 5376

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474  𝒫 cpw 4601

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-pow 5362

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-pw 4603

This theorem is referenced by:  undefval  8257  mapex  8822  pmvalg  8827  fopwdom  9076  pwdom  9125  fineqvlem  9258  fival  9403  fipwuni  9417  hartogslem2  9534  wdompwdom  9569  harwdom  9582  canthwe  10642  canthp1lem2  10644  gchdjuidm  10659  gchpwdom  10661  gchhar  10670  prdsmulr  17401  selvffval  21670  toponsspwpw  22415  mretopd  22587  ordtbaslem  22683  ptcmplem1  23547  isust  23699  blfvalps  23880  carsgval  33290  neibastop2lem  35233  bj-imdirvallem  36049  bj-imdirval2lem  36051  rfovcnvf1od  42740  fsovfd  42748  fsovcnvlem  42749  dssmapnvod  42756  dssmapf1od  42757  ntrneif1o  42811  ntrneicnv  42814  ntrneiel  42817  clsneiel1  42844  neicvgf1o  42850  neicvgnvo  42851  neicvgel1  42855  ntrelmap  42861  clselmap  42863  salexct  45036  psmeasurelem  45172  caragenval  45195  omeunile  45207  0ome  45231  isomennd  45233  afv2ex  45908