Theorem pwexd 5340

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-pw 4558

This theorem is used by:  fabexd  7949  undefval  8294  pmvalg  8857  fopwdom  9104  pwdom  9148  fineqvlem  9257  fival  9404  fipwuni  9418  hartogslem2  9537  wdompwdom  9572  harwdom  9585  canthwe  10736  canthp1lem2  10738  gchdjuidm  10753  gchpwdom  10755  gchhar  10764  prdsmulr  17630  selvffval  22427  toponsspwpw  23240  mretopd  23410  ordtbaslem  23506  ptcmplem1  24371  isust  24523  blfvalps  24702  esplympl  34199  carsgval  34935  abweex  35718  neibastop2lem  37148  bj-imdirvallem  38102  bj-imdirval2lem  38104  rfovcnvf1od  45004  fsovfd  45012  fsovcnvlem  45013  dssmapnvod  45020  dssmapf1od  45021  ntrneif1o  45075  ntrneicnv  45078  ntrneiel  45081  clsneiel1  45108  neicvgf1o  45114  neicvgnvo  45115  neicvgel1  45119  ntrelmap  45125  clselmap  45127  salexct  47344  psmeasurelem  47480  caragenval  47503  omeunile  47515  0ome  47539  isomennd  47541  tmachlem-tpitem  47950  afv2ex  48284  gpgvtx  49141  gpgiedg  49142