This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sspwi

Description: The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024)

Ref Expression
Hypothesis sspwi.1 ⊢ 𝐴 ⊆ 𝐵
Assertion sspwi 𝒫 𝐴 ⊆ 𝒫 𝐵

Proof

Step Hyp Ref Expression
1 sspwi.1 ⊢ 𝐴 ⊆ 𝐵
2 sspw ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
3 1 2 ax-mp ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵