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 18	1 ⊢ (𝜑 → 𝒫 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Vcvv 3454  𝒫 cpw 4561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pow 5335

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-pw 4563

This theorem is used by:  fabexd  7932  undefval  8271  pmvalg  8832  fopwdom  9071  pwdom  9115  fineqvlem  9224  fival  9370  fipwuni  9384  hartogslem2  9503  wdompwdom  9538  harwdom  9551  canthwe  10642  canthp1lem2  10644  gchdjuidm  10659  gchpwdom  10661  gchhar  10670  prdsmulr  17518  selvffval  22280  toponsspwpw  23090  mretopd  23260  ordtbaslem  23356  ptcmplem1  24220  isust  24372  blfvalps  24551  esplympl  33966  carsgval  34702  neibastop2lem  36899  bj-imdirvallem  37852  bj-imdirval2lem  37854  rfovcnvf1od  44758  fsovfd  44766  fsovcnvlem  44767  dssmapnvod  44774  dssmapf1od  44775  ntrneif1o  44829  ntrneicnv  44832  ntrneiel  44835  clsneiel1  44862  neicvgf1o  44868  neicvgnvo  44869  neicvgel1  44873  ntrelmap  44879  clselmap  44881  salexct  47076  psmeasurelem  47212  caragenval  47235  omeunile  47247  0ome  47271  isomennd  47273  afv2ex  47979  gpgvtx  48836  gpgiedg  48837