Description: Quantitative version of ssexg : a subset of an element of a class is an element of the powerclass of the union of that class. (Contributed by BJ, 6-Apr-2024)