Theorem sspwd 4547

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

Syntax hints:   → wi 4   ⊆ wss 3929  𝒫 cpw 4532

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-v 3493  df-in 3936  df-ss 3945  df-pw 4534

This theorem is referenced by:  pweq  4548  pwel  5275  marypha1lem  8890  pwwf  9229  rankpwi  9245  ackbij2lem1  9634  fictb  9660  ssfin2  9735  ssfin3ds  9745  ttukeylem2  9925  hashbcss  16333  isacs1i  16921  mreacs  16922  acsfn  16923  isacs3lem  17769  isacs5lem  17772  tgcmp  22002  imastopn  22321  fgabs  22480  fgtr  22491  trfg  22492  ssufl  22519  alexsubb  22647  cfiluweak  22897  cmetss  23912  minveclem4a  24026  minveclem4  24028  ldsysgenld  31438  neibastop1  33726  neibastop2lem  33727  neibastop2  33728  sstotbnd2  35092  isnacs3  39390  aomclem2  39738  sge0iunmptlemre  42778