Theorem pwexd 5315

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436  𝒫 cpw 4547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-pow 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-pw 4549

This theorem is referenced by:  fabexd  7867  undefval  8206  mapexOLD  8756  pmvalg  8761  fopwdom  8998  pwdom  9042  fineqvlem  9150  fival  9296  fipwuni  9310  hartogslem2  9429  wdompwdom  9464  harwdom  9477  canthwe  10542  canthp1lem2  10544  gchdjuidm  10559  gchpwdom  10561  gchhar  10570  prdsmulr  17363  selvffval  22048  toponsspwpw  22837  mretopd  23007  ordtbaslem  23103  ptcmplem1  23967  isust  24119  blfvalps  24298  esplympl  33588  carsgval  34316  neibastop2lem  36404  bj-imdirvallem  37224  bj-imdirval2lem  37226  rfovcnvf1od  44096  fsovfd  44104  fsovcnvlem  44105  dssmapnvod  44112  dssmapf1od  44113  ntrneif1o  44167  ntrneicnv  44170  ntrneiel  44173  clsneiel1  44200  neicvgf1o  44206  neicvgnvo  44207  neicvgel1  44211  ntrelmap  44217  clselmap  44219  salexct  46431  psmeasurelem  46567  caragenval  46590  omeunile  46602  0ome  46626  isomennd  46628  afv2ex  47313  gpgvtx  48142  gpgiedg  48143