Theorem sspwd 4548

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

Syntax hints:   → wi 4   ⊆ wss 3887  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  pweq  4549  pwel  5304  marypha1lem  9192  pwwf  9565  rankpwi  9581  ackbij2lem1  9975  fictb  10001  ssfin2  10076  ssfin3ds  10086  ttukeylem2  10266  hashbcss  16705  isacs1i  17366  mreacs  17367  acsfn  17368  isacs3lem  18260  isacs5lem  18263  tgcmp  22552  imastopn  22871  fgabs  23030  fgtr  23041  trfg  23042  ssufl  23069  alexsubb  23197  cfiluweak  23447  cmetss  24480  minveclem4a  24594  minveclem4  24596  ldsysgenld  32128  madess  34059  neibastop1  34548  neibastop2lem  34549  neibastop2  34550  sstotbnd2  35932  isnacs3  40532  aomclem2  40880  sge0iunmptlemre  43953