Theorem sspwi 4574

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

Syntax hints:   ⊆ wss 3905  𝒫 cpw 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-pw 4564

This theorem is referenced by:  pwunss  4580  pwundif  4587  pwdom  9113  wdompwdom  9536  rankxplim  9847  hashbclem  14485  incexclem  15886  sscpwex  17867  wunfunc  17953  tsmsres  24301  cfilresi  25454  vitali  25772  sqff1o  27346  ldgenpisyslem1  34553  imambfm  34652  ballotlem2  34879  ttcpwss  37026  dssmapnvod  44746  gneispace  44860  sge0less  47106