Theorem pwexd 5337

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  𝒫 cpw 4566

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 2702  ax-sep 5254  ax-pow 5323

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-pw 4568

This theorem is referenced by:  fabexd  7916  undefval  8258  mapexOLD  8808  pmvalg  8813  fopwdom  9054  pwdom  9099  fineqvlem  9216  fival  9370  fipwuni  9384  hartogslem2  9503  wdompwdom  9538  harwdom  9551  canthwe  10611  canthp1lem2  10613  gchdjuidm  10628  gchpwdom  10630  gchhar  10639  prdsmulr  17429  selvffval  22027  toponsspwpw  22816  mretopd  22986  ordtbaslem  23082  ptcmplem1  23946  isust  24098  blfvalps  24278  carsgval  34301  neibastop2lem  36355  bj-imdirvallem  37175  bj-imdirval2lem  37177  rfovcnvf1od  44000  fsovfd  44008  fsovcnvlem  44009  dssmapnvod  44016  dssmapf1od  44017  ntrneif1o  44071  ntrneicnv  44074  ntrneiel  44077  clsneiel1  44104  neicvgf1o  44110  neicvgnvo  44111  neicvgel1  44115  ntrelmap  44121  clselmap  44123  salexct  46339  psmeasurelem  46475  caragenval  46498  omeunile  46510  0ome  46534  isomennd  46536  afv2ex  47219  gpgvtx  48038  gpgiedg  48039