Theorem pwexd 5334

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447  𝒫 cpw 4563

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-pow 5320

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-pw 4565

This theorem is referenced by:  fabexd  7913  undefval  8255  mapexOLD  8805  pmvalg  8810  fopwdom  9049  pwdom  9093  fineqvlem  9209  fival  9363  fipwuni  9377  hartogslem2  9496  wdompwdom  9531  harwdom  9544  canthwe  10604  canthp1lem2  10606  gchdjuidm  10621  gchpwdom  10623  gchhar  10632  prdsmulr  17422  selvffval  22020  toponsspwpw  22809  mretopd  22979  ordtbaslem  23075  ptcmplem1  23939  isust  24091  blfvalps  24271  carsgval  34294  neibastop2lem  36348  bj-imdirvallem  37168  bj-imdirval2lem  37170  rfovcnvf1od  43993  fsovfd  44001  fsovcnvlem  44002  dssmapnvod  44009  dssmapf1od  44010  ntrneif1o  44064  ntrneicnv  44067  ntrneiel  44070  clsneiel1  44097  neicvgf1o  44103  neicvgnvo  44104  neicvgel1  44108  ntrelmap  44114  clselmap  44116  salexct  46332  psmeasurelem  46468  caragenval  46491  omeunile  46503  0ome  46527  isomennd  46529  afv2ex  47215  gpgvtx  48034  gpgiedg  48035