Theorem sspwd 4579

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

Syntax hints:   → wi 4   ⊆ wss 3917  𝒫 cpw 4566

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-pw 4568

This theorem is referenced by:  pweq  4580  pwel  5339  marypha1lem  9391  pwwf  9767  rankpwi  9783  ackbij2lem1  10178  fictb  10204  ssfin2  10280  ssfin3ds  10290  ttukeylem2  10470  hashbcss  16982  isacs1i  17625  mreacs  17626  acsfn  17627  isacs3lem  18508  isacs5lem  18511  tgcmp  23295  imastopn  23614  fgabs  23773  fgtr  23784  trfg  23785  ssufl  23812  alexsubb  23940  cfiluweak  24189  cmetss  25223  minveclem4a  25337  minveclem4  25339  madess  27795  ldsysgenld  34157  neibastop1  36354  neibastop2lem  36355  neibastop2  36356  sstotbnd2  37775  prjcrv0  42628  isnacs3  42705  aomclem2  43051  sge0iunmptlemre  46420