Theorem sspwi 4544

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 4543	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3	1, 2	ax-mp 5	1 ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵

Syntax hints:   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  pwunss  4550  pwundif  4556  pwdom  8865  wdompwdom  9267  rankxplim  9568  hashbclem  14092  incexclem  15476  sscpwex  17444  wunfunc  17530  wunfuncOLD  17531  tsmsres  23203  cfilresi  24364  vitali  24682  sqff1o  26236  ldgenpisyslem1  32031  imambfm  32129  ballotlem2  32355  dssmapnvod  41517  gneispace  41633  sge0less  43820