Theorem sspwd 4555

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

Syntax hints:   → wi 4   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544

This theorem is referenced by:  pweq  4556  pwel  5320  marypha1lem  9341  pwwf  9726  rankpwi  9742  ackbij2lem1  10135  fictb  10161  ssfin2  10237  ssfin3ds  10247  ttukeylem2  10427  hashbcss  16970  isacs1i  17618  mreacs  17619  acsfn  17620  isacs3lem  18503  isacs5lem  18506  tgcmp  23380  imastopn  23699  fgabs  23858  fgtr  23869  trfg  23870  ssufl  23897  alexsubb  24025  cfiluweak  24273  cmetss  25297  minveclem4a  25411  minveclem4  25413  madess  27876  ldsysgenld  34324  neibastop1  36561  neibastop2lem  36562  neibastop2  36563  sstotbnd2  38113  prjcrv0  43084  isnacs3  43160  aomclem2  43505  sge0iunmptlemre  46865