Theorem pwexd 5349

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459  𝒫 cpw 4575

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-pow 5335

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-pw 4577

This theorem is referenced by:  fabexd  7931  undefval  8273  mapexOLD  8844  pmvalg  8849  fopwdom  9092  pwdom  9141  fineqvlem  9268  fival  9422  fipwuni  9436  hartogslem2  9555  wdompwdom  9590  harwdom  9603  canthwe  10663  canthp1lem2  10665  gchdjuidm  10680  gchpwdom  10682  gchhar  10691  prdsmulr  17471  selvffval  22069  toponsspwpw  22858  mretopd  23028  ordtbaslem  23124  ptcmplem1  23988  isust  24140  blfvalps  24320  carsgval  34281  neibastop2lem  36324  bj-imdirvallem  37144  bj-imdirval2lem  37146  rfovcnvf1od  43975  fsovfd  43983  fsovcnvlem  43984  dssmapnvod  43991  dssmapf1od  43992  ntrneif1o  44046  ntrneicnv  44049  ntrneiel  44052  clsneiel1  44079  neicvgf1o  44085  neicvgnvo  44086  neicvgel1  44090  ntrelmap  44096  clselmap  44098  salexct  46311  psmeasurelem  46447  caragenval  46470  omeunile  46482  0ome  46506  isomennd  46508  afv2ex  47191  gpgvtx  47995  gpgiedg  47996