Theorem sspwd 4565

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

Syntax hints:   → wi 4   ⊆ wss 3899  𝒫 cpw 4552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-pw 4554

This theorem is referenced by:  pweq  4566  pwel  5324  marypha1lem  9334  pwwf  9717  rankpwi  9733  ackbij2lem1  10126  fictb  10152  ssfin2  10228  ssfin3ds  10238  ttukeylem2  10418  hashbcss  16930  isacs1i  17578  mreacs  17579  acsfn  17580  isacs3lem  18463  isacs5lem  18466  tgcmp  23343  imastopn  23662  fgabs  23821  fgtr  23832  trfg  23833  ssufl  23860  alexsubb  23988  cfiluweak  24236  cmetss  25270  minveclem4a  25384  minveclem4  25386  madess  27848  ldsysgenld  34266  neibastop1  36502  neibastop2lem  36503  neibastop2  36504  sstotbnd2  37914  prjcrv0  42818  isnacs3  42894  aomclem2  43239  sge0iunmptlemre  46601