Theorem sspwi 4568

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

This proof depends on syntax axioms:   ⊆ wss 3896  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-pw 4558

This theorem is used by:  pwunss  4575  pwundif  4582  pwdom  9156  wdompwdom  9579  rankxplim  9903  hashbclem  14604  incexclem  16014  sscpwex  17999  wunfunc  18085  tsmsres  24472  cfilresi  25625  vitali  25943  sqff1o  27518  ldgenpisyslem1  34846  imambfm  34944  ballotlem2  35171  ttcpwss  37427  dssmapnvod  45157  gneispace  45271  sge0less  47538