Theorem pwexd 5329

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444  𝒫 cpw 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-pow 5315

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-pw 4561

This theorem is referenced by:  fabexd  7893  undefval  8232  mapexOLD  8782  pmvalg  8787  fopwdom  9026  pwdom  9070  fineqvlem  9185  fival  9339  fipwuni  9353  hartogslem2  9472  wdompwdom  9507  harwdom  9520  canthwe  10580  canthp1lem2  10582  gchdjuidm  10597  gchpwdom  10599  gchhar  10608  prdsmulr  17398  selvffval  22053  toponsspwpw  22842  mretopd  23012  ordtbaslem  23108  ptcmplem1  23972  isust  24124  blfvalps  24304  carsgval  34287  neibastop2lem  36341  bj-imdirvallem  37161  bj-imdirval2lem  37163  rfovcnvf1od  43986  fsovfd  43994  fsovcnvlem  43995  dssmapnvod  44002  dssmapf1od  44003  ntrneif1o  44057  ntrneicnv  44060  ntrneiel  44063  clsneiel1  44090  neicvgf1o  44096  neicvgnvo  44097  neicvgel1  44101  ntrelmap  44107  clselmap  44109  salexct  46325  psmeasurelem  46461  caragenval  46484  omeunile  46496  0ome  46520  isomennd  46522  afv2ex  47208  gpgvtx  48027  gpgiedg  48028