Theorem sspwd 4618

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

Syntax hints:   → wi 4   ⊆ wss 3963  𝒫 cpw 4605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-pw 4607

This theorem is referenced by:  pweq  4619  pwel  5387  marypha1lem  9471  pwwf  9845  rankpwi  9861  ackbij2lem1  10256  fictb  10282  ssfin2  10358  ssfin3ds  10368  ttukeylem2  10548  hashbcss  17038  isacs1i  17702  mreacs  17703  acsfn  17704  isacs3lem  18600  isacs5lem  18603  tgcmp  23425  imastopn  23744  fgabs  23903  fgtr  23914  trfg  23915  ssufl  23942  alexsubb  24070  cfiluweak  24320  cmetss  25364  minveclem4a  25478  minveclem4  25480  madess  27930  ldsysgenld  34141  neibastop1  36342  neibastop2lem  36343  neibastop2  36344  sstotbnd2  37761  prjcrv0  42620  isnacs3  42698  aomclem2  43044  sge0iunmptlemre  46371