Theorem pwexd 5341

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

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

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 2732  ax-sep 5249  ax-pow 5327

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-pw 4559

This theorem is used by:  fabexd  7933  undefval  8273  pmvalg  8836  fopwdom  9083  pwdom  9127  fineqvlem  9236  fival  9382  fipwuni  9396  hartogslem2  9515  wdompwdom  9550  harwdom  9563  canthwe  10693  canthp1lem2  10695  gchdjuidm  10710  gchpwdom  10712  gchhar  10721  prdsmulr  17577  selvffval  22374  toponsspwpw  23187  mretopd  23357  ordtbaslem  23453  ptcmplem1  24318  isust  24470  blfvalps  24649  esplympl  34118  carsgval  34855  neibastop2lem  37064  bj-imdirvallem  38015  bj-imdirval2lem  38017  rfovcnvf1od  44942  fsovfd  44950  fsovcnvlem  44951  dssmapnvod  44958  dssmapf1od  44959  ntrneif1o  45013  ntrneicnv  45016  ntrneiel  45019  clsneiel1  45046  neicvgf1o  45052  neicvgnvo  45053  neicvgel1  45057  ntrelmap  45063  clselmap  45065  salexct  47260  psmeasurelem  47396  caragenval  47419  omeunile  47431  0ome  47455  isomennd  47457  tmachlem-tpitem  47866  afv2ex  48200  gpgvtx  49057  gpgiedg  49058