Theorem sspwd 4616

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

Syntax hints:   → wi 4   ⊆ wss 3949  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  pweq  4617  pwel  5380  marypha1lem  9432  pwwf  9806  rankpwi  9822  ackbij2lem1  10218  fictb  10244  ssfin2  10319  ssfin3ds  10329  ttukeylem2  10509  hashbcss  16943  isacs1i  17607  mreacs  17608  acsfn  17609  isacs3lem  18501  isacs5lem  18504  tgcmp  23127  imastopn  23446  fgabs  23605  fgtr  23616  trfg  23617  ssufl  23644  alexsubb  23772  cfiluweak  24022  cmetss  25066  minveclem4a  25180  minveclem4  25182  madess  27606  ldsysgenld  33454  neibastop1  35549  neibastop2lem  35550  neibastop2  35551  sstotbnd2  36947  prjcrv0  41679  isnacs3  41752  aomclem2  42101  sge0iunmptlemre  45431