Theorem sspwd 4572

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

Syntax hints:   → wi 4   ⊆ wss 3911  𝒫 cpw 4559

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

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 3446  df-ss 3928  df-pw 4561

This theorem is referenced by:  pweq  4573  pwel  5331  marypha1lem  9360  pwwf  9736  rankpwi  9752  ackbij2lem1  10147  fictb  10173  ssfin2  10249  ssfin3ds  10259  ttukeylem2  10439  hashbcss  16951  isacs1i  17598  mreacs  17599  acsfn  17600  isacs3lem  18483  isacs5lem  18486  tgcmp  23321  imastopn  23640  fgabs  23799  fgtr  23810  trfg  23811  ssufl  23838  alexsubb  23966  cfiluweak  24215  cmetss  25249  minveclem4a  25363  minveclem4  25365  madess  27825  ldsysgenld  34143  neibastop1  36340  neibastop2lem  36341  neibastop2  36342  sstotbnd2  37761  prjcrv0  42614  isnacs3  42691  aomclem2  43037  sge0iunmptlemre  46406