Theorem sspwd 4575

Description: The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.)

Hypothesis

Ref	Expression
sspwd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
sspwd	⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Proof of Theorem sspwd

Step	Hyp	Ref	Expression
1		sspwd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sspw 4573	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3905  𝒫 cpw 4562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-pw 4564

This theorem is used by:  pweq  4576  pwel  5352  pwuninel  8267  marypha1lem  9389  pwwf  9775  rankpwi  9791  ackbij2lem1  10206  fictb  10232  ssfin2  10308  ssfin3ds  10318  ttukeylem2  10498  hashbcss  17068  isacs1i  17717  mreacs  17718  acsfn  17719  isacs3lem  18602  isacs5lem  18605  tgcmp  23567  imastopn  23886  fgabs  24045  fgtr  24056  trfg  24057  ssufl  24084  alexsubb  24212  cfiluweak  24460  cmetss  25484  minveclem4a  25598  minveclem4  25600  madess  28068  ldsysgenld  34559  neibastop1  36898  neibastop2lem  36899  neibastop2  36900  sstotbnd2  38453  prjcrv0  43393  isnacs3  43469  aomclem2  43810  sge0iunmptlemre  47157