Theorem pwexd 5351

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3461  𝒫 cpw 4565

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 5259  ax-pow 5337

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 3463  df-ss 3928  df-pw 4567

This theorem is referenced by:  fabexd  7934  undefval  8273  pmvalg  8834  fopwdom  9073  pwdom  9117  fineqvlem  9226  fival  9372  fipwuni  9386  hartogslem2  9505  wdompwdom  9540  harwdom  9553  canthwe  10636  canthp1lem2  10638  gchdjuidm  10653  gchpwdom  10655  gchhar  10664  prdsmulr  17512  selvffval  22238  toponsspwpw  23048  mretopd  23218  ordtbaslem  23314  ptcmplem1  24178  isust  24330  blfvalps  24509  esplympl  33902  carsgval  34638  neibastop2lem  36794  bj-imdirvallem  37747  bj-imdirval2lem  37749  rfovcnvf1od  44657  fsovfd  44665  fsovcnvlem  44666  dssmapnvod  44673  dssmapf1od  44674  ntrneif1o  44728  ntrneicnv  44731  ntrneiel  44734  clsneiel1  44761  neicvgf1o  44767  neicvgnvo  44768  neicvgel1  44772  ntrelmap  44778  clselmap  44780  salexct  46975  psmeasurelem  47111  caragenval  47134  omeunile  47146  0ome  47170  isomennd  47172  afv2ex  47875  gpgvtx  48732  gpgiedg  48733