Theorem sspwd 4635

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

Syntax hints:   → wi 4   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624

This theorem is referenced by:  pweq  4636  pwel  5399  marypha1lem  9502  pwwf  9876  rankpwi  9892  ackbij2lem1  10287  fictb  10313  ssfin2  10389  ssfin3ds  10399  ttukeylem2  10579  hashbcss  17051  isacs1i  17715  mreacs  17716  acsfn  17717  isacs3lem  18612  isacs5lem  18615  tgcmp  23430  imastopn  23749  fgabs  23908  fgtr  23919  trfg  23920  ssufl  23947  alexsubb  24075  cfiluweak  24325  cmetss  25369  minveclem4a  25483  minveclem4  25485  madess  27933  ldsysgenld  34124  neibastop1  36325  neibastop2lem  36326  neibastop2  36327  sstotbnd2  37734  prjcrv0  42588  isnacs3  42666  aomclem2  43012  sge0iunmptlemre  46336