Theorem sspwd 4568

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

Syntax hints:   → wi 4   ⊆ wss 3902  𝒫 cpw 4555

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 3443  df-ss 3919  df-pw 4557

This theorem is referenced by:  pweq  4569  pwel  5327  marypha1lem  9340  pwwf  9723  rankpwi  9739  ackbij2lem1  10132  fictb  10158  ssfin2  10234  ssfin3ds  10244  ttukeylem2  10424  hashbcss  16936  isacs1i  17584  mreacs  17585  acsfn  17586  isacs3lem  18469  isacs5lem  18472  tgcmp  23349  imastopn  23668  fgabs  23827  fgtr  23838  trfg  23839  ssufl  23866  alexsubb  23994  cfiluweak  24242  cmetss  25276  minveclem4a  25390  minveclem4  25392  madess  27866  ldsysgenld  34319  neibastop1  36555  neibastop2lem  36556  neibastop2  36557  sstotbnd2  37977  prjcrv0  42943  isnacs3  43019  aomclem2  43364  sge0iunmptlemre  46726