Theorem pwexd 5245

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441  𝒫 cpw 4497

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-pow 5231

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  undefval  7925  mapex  8395  pmvalg  8400  fopwdom  8608  pwdom  8653  fineqvlem  8716  fival  8860  fipwuni  8874  hartogslem2  8991  wdompwdom  9026  harwdom  9039  canthwe  10062  canthp1lem2  10064  gchdjuidm  10079  gchpwdom  10081  gchhar  10090  prdsmulr  16724  sylow2a  18736  selvffval  20788  toponsspwpw  21527  mretopd  21697  ordtbaslem  21793  ptcmplem1  22657  isust  22809  blfvalps  22990  carsgval  31671  neibastop2lem  33821  bj-imdirvallem  34595  bj-imdirval2lem  34597  rfovcnvf1od  40705  fsovfd  40713  fsovcnvlem  40714  dssmapnvod  40721  dssmapf1od  40722  ntrneif1o  40778  ntrneicnv  40781  ntrneiel  40784  clsneiel1  40811  neicvgf1o  40817  neicvgnvo  40818  neicvgel1  40822  ntrelmap  40828  clselmap  40830  salexct  42974  psmeasurelem  43109  caragenval  43132  omeunile  43144  0ome  43168  isomennd  43170  afv2ex  43770