Description: The powerclass preserves inclusion. See sspwb for the biconditional version. (Contributed by NM, 13-Oct-1996) Extract forward implication of sspwb since it requires fewer axioms. (Revised by BJ, 13-Apr-2024)