Theorem pwexd 5348

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453  𝒫 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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pow 5334

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-pw 4562

This theorem is used by:  fabexd  7937  undefval  8278  pmvalg  8839  fopwdom  9086  pwdom  9130  fineqvlem  9239  fival  9385  fipwuni  9399  hartogslem2  9518  wdompwdom  9553  harwdom  9566  canthwe  10663  canthp1lem2  10665  gchdjuidm  10680  gchpwdom  10682  gchhar  10691  prdsmulr  17548  selvffval  22335  toponsspwpw  23148  mretopd  23318  ordtbaslem  23414  ptcmplem1  24279  isust  24431  blfvalps  24610  esplympl  34064  carsgval  34801  neibastop2lem  36966  bj-imdirvallem  37919  bj-imdirval2lem  37921  rfovcnvf1od  44831  fsovfd  44839  fsovcnvlem  44840  dssmapnvod  44847  dssmapf1od  44848  ntrneif1o  44902  ntrneicnv  44905  ntrneiel  44908  clsneiel1  44935  neicvgf1o  44941  neicvgnvo  44942  neicvgel1  44946  ntrelmap  44952  clselmap  44954  salexct  47149  psmeasurelem  47285  caragenval  47308  omeunile  47320  0ome  47344  isomennd  47346  tmachlem-tpitem  47755  afv2ex  48089  gpgvtx  48946  gpgiedg  48947