Theorem sspwi 4569

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

This proof depends on syntax axioms:   ⊆ wss 3899  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559

This theorem is used by:  pwunss  4575  pwundif  4582  pwdom  9148  wdompwdom  9572  rankxplim  9896  hashbclem  14597  incexclem  16005  sscpwex  17990  wunfunc  18076  tsmsres  24463  cfilresi  25616  vitali  25934  sqff1o  27509  ldgenpisyslem1  34796  imambfm  34894  ballotlem2  35121  ttcpwss  37303  dssmapnvod  45019  gneispace  45133  sge0less  47401