Theorem sspwd 4608

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

Syntax hints:   → wi 4   ⊆ wss 3941  𝒫 cpw 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3948  df-ss 3958  df-pw 4597

This theorem is referenced by:  pweq  4609  pwel  5370  marypha1lem  9425  pwwf  9799  rankpwi  9815  ackbij2lem1  10211  fictb  10237  ssfin2  10312  ssfin3ds  10322  ttukeylem2  10502  hashbcss  16938  isacs1i  17602  mreacs  17603  acsfn  17604  isacs3lem  18499  isacs5lem  18502  tgcmp  23229  imastopn  23548  fgabs  23707  fgtr  23718  trfg  23719  ssufl  23746  alexsubb  23874  cfiluweak  24124  cmetss  25168  minveclem4a  25282  minveclem4  25284  madess  27722  ldsysgenld  33650  neibastop1  35735  neibastop2lem  35736  neibastop2  35737  sstotbnd2  37136  prjcrv0  41889  isnacs3  41962  aomclem2  42311  sge0iunmptlemre  45641