Theorem sspwd 4580

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 4578	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3913  𝒫 cpw 4567

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

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 3465  df-ss 3930  df-pw 4569

This theorem is referenced by:  pweq  4581  pwel  5353  pwuninel  8271  marypha1lem  9393  pwwf  9779  rankpwi  9795  ackbij2lem1  10201  fictb  10227  ssfin2  10304  ssfin3ds  10314  ttukeylem2  10494  hashbcss  17064  isacs1i  17713  mreacs  17714  acsfn  17715  isacs3lem  18598  isacs5lem  18601  tgcmp  23527  imastopn  23846  fgabs  24005  fgtr  24016  trfg  24017  ssufl  24044  alexsubb  24172  cfiluweak  24420  cmetss  25444  minveclem4a  25558  minveclem4  25560  madess  28025  ldsysgenld  34495  neibastop1  36793  neibastop2lem  36794  neibastop2  36795  sstotbnd2  38347  prjcrv0  43291  isnacs3  43367  aomclem2  43708  sge0iunmptlemre  47055