Theorem sspwd 4554

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

Syntax hints:   → wi 4   ⊆ wss 3889  𝒫 cpw 4541

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543

This theorem is referenced by:  pweq  4555  pwel  5323  marypha1lem  9346  pwwf  9731  rankpwi  9747  ackbij2lem1  10140  fictb  10166  ssfin2  10242  ssfin3ds  10252  ttukeylem2  10432  hashbcss  16975  isacs1i  17623  mreacs  17624  acsfn  17625  isacs3lem  18508  isacs5lem  18511  tgcmp  23366  imastopn  23685  fgabs  23844  fgtr  23855  trfg  23856  ssufl  23883  alexsubb  24011  cfiluweak  24259  cmetss  25283  minveclem4a  25397  minveclem4  25399  madess  27858  ldsysgenld  34304  neibastop1  36541  neibastop2lem  36542  neibastop2  36543  sstotbnd2  38095  prjcrv0  43066  isnacs3  43142  aomclem2  43483  sge0iunmptlemre  46843