Theorem sspwd 4570

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

Syntax hints:   → wi 4   ⊆ wss 3906  𝒫 cpw 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-pw 4559

This theorem is referenced by:  pweq  4571  pwel  5340  pwuninel  8257  marypha1lem  9381  pwwf  9767  rankpwi  9783  ackbij2lem1  10176  fictb  10202  ssfin2  10279  ssfin3ds  10289  ttukeylem2  10469  hashbcss  17042  isacs1i  17691  mreacs  17692  acsfn  17693  isacs3lem  18576  isacs5lem  18579  tgcmp  23463  imastopn  23782  fgabs  23941  fgtr  23952  trfg  23953  ssufl  23980  alexsubb  24108  cfiluweak  24356  cmetss  25380  minveclem4a  25494  minveclem4  25496  madess  27961  ldsysgenld  34459  neibastop1  36724  neibastop2lem  36725  neibastop2  36726  sstotbnd2  38278  prjcrv0  43220  isnacs3  43296  aomclem2  43637  sge0iunmptlemre  46994