Theorem pwexd 5279

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3494  𝒫 cpw 4538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-pow 5265

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496  df-in 3942  df-ss 3951  df-pw 4540

This theorem is referenced by:  undefval  7941  mapex  8411  pmvalg  8416  fopwdom  8624  pwdom  8668  fineqvlem  8731  fival  8875  fipwuni  8889  hartogslem2  9006  wdompwdom  9041  harwdom  9053  canthwe  10072  canthp1lem2  10074  gchdjuidm  10089  gchpwdom  10091  gchhar  10100  wrdexgOLD  13871  prdsmulr  16731  sylow2a  18743  selvffval  20328  toponsspwpw  21529  mretopd  21699  ordtbaslem  21795  ptcmplem1  22659  isust  22811  blfvalps  22992  carsgval  31561  neibastop2lem  33708  bj-imdirval  34471  bj-imdirval2  34472  rfovcnvf1od  40348  fsovfd  40356  fsovcnvlem  40357  dssmapnvod  40364  dssmapf1od  40365  ntrneif1o  40423  ntrneicnv  40426  ntrneiel  40429  clsneiel1  40456  neicvgf1o  40462  neicvgnvo  40463  neicvgel1  40467  ntrelmap  40473  clselmap  40475  salexct  42616  psmeasurelem  42751  caragenval  42774  omeunile  42786  0ome  42810  isomennd  42812  afv2ex  43412