Theorem pwexd 5271

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3493  𝒫 cpw 4537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-pow 5257

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-v 3495  df-in 3941  df-ss 3950  df-pw 4539

This theorem is referenced by:  undefval  7934  mapex  8404  pmvalg  8409  fopwdom  8617  pwdom  8661  fineqvlem  8724  fival  8868  fipwuni  8882  hartogslem2  8999  wdompwdom  9034  harwdom  9046  canthwe  10065  canthp1lem2  10067  gchdjuidm  10082  gchpwdom  10084  gchhar  10093  wrdexgOLD  13864  prdsmulr  16724  sylow2a  18736  selvffval  20321  toponsspwpw  21522  mretopd  21692  ordtbaslem  21788  ptcmplem1  22652  isust  22804  blfvalps  22985  carsgval  31554  neibastop2lem  33701  bj-imdirval  34464  bj-imdirval2  34465  rfovcnvf1od  40341  fsovfd  40349  fsovcnvlem  40350  dssmapnvod  40357  dssmapf1od  40358  ntrneif1o  40416  ntrneicnv  40419  ntrneiel  40422  clsneiel1  40449  neicvgf1o  40455  neicvgnvo  40456  neicvgel1  40460  ntrelmap  40466  clselmap  40468  salexct  42608  psmeasurelem  42743  caragenval  42766  omeunile  42778  0ome  42802  isomennd  42804  afv2ex  43404