Theorem sspwd 4577

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3906  𝒫 cpw 4564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-pw 4566

This theorem is used by:  pweq  4578  pwel  5354  pwuninel  8278  marypha1lem  9401  pwwf  9787  rankpwi  9803  ackbij2lem1  10218  fictb  10244  ssfin2  10320  ssfin3ds  10330  ttukeylem2  10510  hashbcss  17091  isacs1i  17740  mreacs  17741  acsfn  17742  isacs3lem  18625  isacs5lem  18628  tgcmp  23613  imastopn  23933  fgabs  24092  fgtr  24103  trfg  24104  ssufl  24131  alexsubb  24259  cfiluweak  24507  cmetss  25531  minveclem4a  25645  minveclem4  25647  madess  28115  ldsysgenld  34620  neibastop1  36932  neibastop2lem  36933  neibastop2  36934  sstotbnd2  38488  prjcrv0  43443  isnacs3  43519  aomclem2  43860  sge0iunmptlemre  47207