Theorem sspwd 4512

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

Syntax hints:   → wi 4   ⊆ wss 3881  𝒫 cpw 4497

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  pweq  4513  pwel  5247  marypha1lem  8881  pwwf  9220  rankpwi  9236  ackbij2lem1  9630  fictb  9656  ssfin2  9731  ssfin3ds  9741  ttukeylem2  9921  hashbcss  16330  isacs1i  16920  mreacs  16921  acsfn  16922  isacs3lem  17768  isacs5lem  17771  tgcmp  22006  imastopn  22325  fgabs  22484  fgtr  22495  trfg  22496  ssufl  22523  alexsubb  22651  cfiluweak  22901  cmetss  23920  minveclem4a  24034  minveclem4  24036  ldsysgenld  31529  neibastop1  33820  neibastop2lem  33821  neibastop2  33822  sstotbnd2  35212  isnacs3  39651  aomclem2  39999  sge0iunmptlemre  43054