Theorem sspwd 4545

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

Syntax hints:   → wi 4   ⊆ wss 3885  𝒫 cpw 4532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-pw 4534

This theorem is referenced by:  pweq  4546  pwel  5313  marypha1lem  9340  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  23388  imastopn  23707  fgabs  23866  fgtr  23877  trfg  23878  ssufl  23905  alexsubb  24033  cfiluweak  24281  cmetss  25305  minveclem4a  25419  minveclem4  25421  madess  27880  ldsysgenld  34356  neibastop1  36602  neibastop2lem  36603  neibastop2  36604  sstotbnd2  38156  prjcrv0  43098  isnacs3  43174  aomclem2  43515  sge0iunmptlemre  46872