Theorem pwexd 5397

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pow 5383

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624

This theorem is referenced by:  fabexd  7975  undefval  8317  mapexOLD  8890  pmvalg  8895  fopwdom  9146  pwdom  9195  fineqvlem  9325  fival  9481  fipwuni  9495  hartogslem2  9612  wdompwdom  9647  harwdom  9660  canthwe  10720  canthp1lem2  10722  gchdjuidm  10737  gchpwdom  10739  gchhar  10748  prdsmulr  17519  selvffval  22160  toponsspwpw  22949  mretopd  23121  ordtbaslem  23217  ptcmplem1  24081  isust  24233  blfvalps  24414  carsgval  34268  neibastop2lem  36326  bj-imdirvallem  37146  bj-imdirval2lem  37148  rfovcnvf1od  43966  fsovfd  43974  fsovcnvlem  43975  dssmapnvod  43982  dssmapf1od  43983  ntrneif1o  44037  ntrneicnv  44040  ntrneiel  44043  clsneiel1  44070  neicvgf1o  44076  neicvgnvo  44077  neicvgel1  44081  ntrelmap  44087  clselmap  44089  salexct  46255  psmeasurelem  46391  caragenval  46414  omeunile  46426  0ome  46450  isomennd  46452  afv2ex  47129