Theorem sspwd 4615

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

Syntax hints:   → wi 4   ⊆ wss 3948  𝒫 cpw 4602

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  pweq  4616  pwel  5379  marypha1lem  9427  pwwf  9801  rankpwi  9817  ackbij2lem1  10213  fictb  10239  ssfin2  10314  ssfin3ds  10324  ttukeylem2  10504  hashbcss  16936  isacs1i  17600  mreacs  17601  acsfn  17602  isacs3lem  18494  isacs5lem  18497  tgcmp  22904  imastopn  23223  fgabs  23382  fgtr  23393  trfg  23394  ssufl  23421  alexsubb  23549  cfiluweak  23799  cmetss  24832  minveclem4a  24946  minveclem4  24948  madess  27368  ldsysgenld  33153  neibastop1  35239  neibastop2lem  35240  neibastop2  35241  sstotbnd2  36637  prjcrv0  41376  isnacs3  41438  aomclem2  41787  sge0iunmptlemre  45121