Theorem pwexd 5378

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-pow 5364

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  undefval  8261  mapex  8826  pmvalg  8831  fopwdom  9080  pwdom  9129  fineqvlem  9262  fival  9407  fipwuni  9421  hartogslem2  9538  wdompwdom  9573  harwdom  9586  canthwe  10646  canthp1lem2  10648  gchdjuidm  10663  gchpwdom  10665  gchhar  10674  prdsmulr  17405  selvffval  21679  toponsspwpw  22424  mretopd  22596  ordtbaslem  22692  ptcmplem1  23556  isust  23708  blfvalps  23889  carsgval  33302  neibastop2lem  35245  bj-imdirvallem  36061  bj-imdirval2lem  36063  rfovcnvf1od  42755  fsovfd  42763  fsovcnvlem  42764  dssmapnvod  42771  dssmapf1od  42772  ntrneif1o  42826  ntrneicnv  42829  ntrneiel  42832  clsneiel1  42859  neicvgf1o  42865  neicvgnvo  42866  neicvgel1  42870  ntrelmap  42876  clselmap  42878  salexct  45050  psmeasurelem  45186  caragenval  45209  omeunile  45221  0ome  45245  isomennd  45247  afv2ex  45922