Theorem sspwd 4576

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

Syntax hints:   → wi 4   ⊆ wss 3914  𝒫 cpw 4563

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 3449  df-ss 3931  df-pw 4565

This theorem is referenced by:  pweq  4577  pwel  5336  marypha1lem  9384  pwwf  9760  rankpwi  9776  ackbij2lem1  10171  fictb  10197  ssfin2  10273  ssfin3ds  10283  ttukeylem2  10463  hashbcss  16975  isacs1i  17618  mreacs  17619  acsfn  17620  isacs3lem  18501  isacs5lem  18504  tgcmp  23288  imastopn  23607  fgabs  23766  fgtr  23777  trfg  23778  ssufl  23805  alexsubb  23933  cfiluweak  24182  cmetss  25216  minveclem4a  25330  minveclem4  25332  madess  27788  ldsysgenld  34150  neibastop1  36347  neibastop2lem  36348  neibastop2  36349  sstotbnd2  37768  prjcrv0  42621  isnacs3  42698  aomclem2  43044  sge0iunmptlemre  46413