Theorem pwexd 5373

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

Syntax hints:   → wi 4   ∈ wcel 2099  Vcvv 3470  𝒫 cpw 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5293  ax-pow 5359

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952  df-ss 3962  df-pw 4600

This theorem is referenced by:  undefval  8275  mapex  8844  pmvalg  8849  fopwdom  9098  pwdom  9147  fineqvlem  9280  fival  9429  fipwuni  9443  hartogslem2  9560  wdompwdom  9595  harwdom  9608  canthwe  10668  canthp1lem2  10670  gchdjuidm  10685  gchpwdom  10687  gchhar  10696  prdsmulr  17434  selvffval  22052  toponsspwpw  22817  mretopd  22989  ordtbaslem  23085  ptcmplem1  23949  isust  24101  blfvalps  24282  carsgval  33917  neibastop2lem  35838  bj-imdirvallem  36653  bj-imdirval2lem  36655  rfovcnvf1od  43428  fsovfd  43436  fsovcnvlem  43437  dssmapnvod  43444  dssmapf1od  43445  ntrneif1o  43499  ntrneicnv  43502  ntrneiel  43505  clsneiel1  43532  neicvgf1o  43538  neicvgnvo  43539  neicvgel1  43543  ntrelmap  43549  clselmap  43551  salexct  45716  psmeasurelem  45852  caragenval  45875  omeunile  45887  0ome  45911  isomennd  45913  afv2ex  46588