Theorem sspwd 4564

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

Syntax hints:   → wi 4   ⊆ wss 3903  𝒫 cpw 4551

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-pw 4553

This theorem is referenced by:  pweq  4565  pwel  5320  marypha1lem  9323  pwwf  9703  rankpwi  9719  ackbij2lem1  10112  fictb  10138  ssfin2  10214  ssfin3ds  10224  ttukeylem2  10404  hashbcss  16916  isacs1i  17563  mreacs  17564  acsfn  17565  isacs3lem  18448  isacs5lem  18451  tgcmp  23286  imastopn  23605  fgabs  23764  fgtr  23775  trfg  23776  ssufl  23803  alexsubb  23931  cfiluweak  24180  cmetss  25214  minveclem4a  25328  minveclem4  25330  madess  27790  ldsysgenld  34133  neibastop1  36343  neibastop2lem  36344  neibastop2  36345  sstotbnd2  37764  prjcrv0  42616  isnacs3  42693  aomclem2  43038  sge0iunmptlemre  46406