Theorem sspwi 4583

Description: The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.)

Hypothesis

Ref	Expression
sspwi.1	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
sspwi	⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵

Proof of Theorem sspwi

Step	Hyp	Ref	Expression
1		sspwi.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sspw 4582	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3	1, 2	ax-mp 5	1 ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵

Syntax hints:   ⊆ wss 3922  𝒫 cpw 4571

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3457  df-ss 3939  df-pw 4573

This theorem is referenced by:  pwunss  4589  pwundif  4595  pwdom  9106  wdompwdom  9549  rankxplim  9850  hashbclem  14427  incexclem  15809  sscpwex  17783  wunfunc  17869  tsmsres  24037  cfilresi  25202  vitali  25521  sqff1o  27099  ldgenpisyslem1  34161  imambfm  34261  ballotlem2  34488  dssmapnvod  43981  gneispace  44095  sge0less  46363