Theorem pwexd 5353

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pow 5339

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-pw 4569

This theorem is referenced by:  fabexd  7936  undefval  8275  pmvalg  8836  fopwdom  9075  pwdom  9119  fineqvlem  9228  fival  9374  fipwuni  9388  hartogslem2  9507  wdompwdom  9542  harwdom  9555  canthwe  10638  canthp1lem2  10640  gchdjuidm  10655  gchpwdom  10657  gchhar  10666  prdsmulr  17514  selvffval  22240  toponsspwpw  23050  mretopd  23220  ordtbaslem  23316  ptcmplem1  24180  isust  24332  blfvalps  24511  esplympl  33904  carsgval  34640  neibastop2lem  36796  bj-imdirvallem  37749  bj-imdirval2lem  37751  rfovcnvf1od  44659  fsovfd  44667  fsovcnvlem  44668  dssmapnvod  44675  dssmapf1od  44676  ntrneif1o  44730  ntrneicnv  44733  ntrneiel  44736  clsneiel1  44763  neicvgf1o  44769  neicvgnvo  44770  neicvgel1  44774  ntrelmap  44780  clselmap  44782  salexct  46977  psmeasurelem  47113  caragenval  47136  omeunile  47148  0ome  47172  isomennd  47174  afv2ex  47877  gpgvtx  48734  gpgiedg  48735