Theorem sspwd 4569

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

Syntax hints:   → wi 4   ⊆ wss 3903  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-pw 4558

This theorem is referenced by:  pweq  4570  pwel  5330  marypha1lem  9350  pwwf  9733  rankpwi  9749  ackbij2lem1  10142  fictb  10168  ssfin2  10244  ssfin3ds  10254  ttukeylem2  10434  hashbcss  16946  isacs1i  17594  mreacs  17595  acsfn  17596  isacs3lem  18479  isacs5lem  18482  tgcmp  23362  imastopn  23681  fgabs  23840  fgtr  23851  trfg  23852  ssufl  23879  alexsubb  24007  cfiluweak  24255  cmetss  25289  minveclem4a  25403  minveclem4  25405  madess  27879  ldsysgenld  34344  neibastop1  36581  neibastop2lem  36582  neibastop2  36583  sstotbnd2  38054  prjcrv0  43020  isnacs3  43096  aomclem2  43441  sge0iunmptlemre  46802