Theorem sspwi 4634

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

Syntax hints:   ⊆ 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:  pwunss  4640  pwundif  4646  pwdom  9195  wdompwdom  9647  rankxplim  9948  hashbclem  14501  incexclem  15884  sscpwex  17876  wunfunc  17965  wunfuncOLD  17966  tsmsres  24173  cfilresi  25348  vitali  25667  sqff1o  27243  ldgenpisyslem1  34127  imambfm  34227  ballotlem2  34453  dssmapnvod  43982  gneispace  44096  sge0less  46313