Theorem sspwd 4545

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

Syntax hints:   → wi 4   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  pweq  4546  pwel  5299  marypha1lem  9122  pwwf  9496  rankpwi  9512  ackbij2lem1  9906  fictb  9932  ssfin2  10007  ssfin3ds  10017  ttukeylem2  10197  hashbcss  16633  isacs1i  17283  mreacs  17284  acsfn  17285  isacs3lem  18175  isacs5lem  18178  tgcmp  22460  imastopn  22779  fgabs  22938  fgtr  22949  trfg  22950  ssufl  22977  alexsubb  23105  cfiluweak  23355  cmetss  24385  minveclem4a  24499  minveclem4  24501  ldsysgenld  32028  madess  33986  neibastop1  34475  neibastop2lem  34476  neibastop2  34477  sstotbnd2  35859  isnacs3  40448  aomclem2  40796  sge0iunmptlemre  43843