Theorem pwexd 5345

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pow 5331

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562

This theorem is used by:  fabexd  7970  undefval  8319  pmvalg  8882  fopwdom  9129  pwdom  9173  fineqvlem  9282  fival  9428  fipwuni  9442  hartogslem2  9561  wdompwdom  9596  harwdom  9609  canthwe  10760  canthp1lem2  10762  gchdjuidm  10777  gchpwdom  10779  gchhar  10788  prdsmulr  17656  acsmapd  18754  selvffval  22454  toponsspwpw  23267  mretopd  23437  ordtbaslem  23533  ptcmplem1  24398  isust  24550  blfvalps  24729  esplympl  34266  carsgval  35002  abweex  35798  neibastop2lem  37325  bj-imdirvallem  38292  bj-imdirval2lem  38294  rfovcnvf1od  45194  fsovfd  45202  fsovcnvlem  45203  dssmapnvod  45210  dssmapf1od  45211  ntrneif1o  45265  ntrneicnv  45268  ntrneiel  45271  clsneiel1  45298  neicvgf1o  45304  neicvgnvo  45305  neicvgel1  45309  ntrelmap  45315  clselmap  45317  salexct  47547  psmeasurelem  47683  caragenval  47706  omeunile  47718  0ome  47742  isomennd  47744  tmachlem-tpitem  48153  afv2ex  48487  gpgvtx  49344  gpgiedg  49345