Theorem sspwd 4558

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

Syntax hints:   → wi 4   ⊆ wss 3895  𝒫 cpw 4545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-v 3446  df-ss 3912  df-pw 4547

This theorem is referenced by:  pweq  4559  pwel  5328  pwuninel  8239  marypha1lem  9365  pwwf  9751  rankpwi  9767  ackbij2lem1  10160  fictb  10186  ssfin2  10263  ssfin3ds  10273  ttukeylem2  10453  hashbcss  17012  isacs1i  17661  mreacs  17662  acsfn  17663  isacs3lem  18546  isacs5lem  18549  tgcmp  23430  imastopn  23749  fgabs  23908  fgtr  23919  trfg  23920  ssufl  23947  alexsubb  24075  cfiluweak  24323  cmetss  25347  minveclem4a  25461  minveclem4  25463  madess  27925  ldsysgenld  34401  neibastop1  36657  neibastop2lem  36658  neibastop2  36659  sstotbnd2  38211  prjcrv0  43153  isnacs3  43229  aomclem2  43570  sge0iunmptlemre  46927