**Description: **Define the subsets class
or the class of all subset relations. Similar
to definitions of epsilon relation (df-eprel 5163) and identity relation
(df-id 5158) classes. Subset relation class and Scott
Fenton's subset
class df-sset 32300 are the same: S = SSet (compare dfssr2 34589 with
df-sset 32300, cf. comment of df-xrn 34473), the only reason we do not use
dfssr2 34589 as the base definition of the subsets class
is the way we
defined the epsilon relation and the identity relation classes.
The binary relation on the class of all subsets and the subclass
relationship (df-ss 3737) are the same, that is,
(𝐴
S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, cf. brssr 34591. Yet in
general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for
sets, cf. the comment of df-ss 3737. The only exception (aside from
directly investigating the class S e.g. in relssr 34590 or in
extssr 34599) is when we have a specific purpose with its
usage, like in
case of df-refs 34600 vs. df-cnvrefs 34613, where we need S to
define the
class of reflexive sets in order to be able to define the class of
converse reflexive sets with the help of the converse of S.
The subsets class S has another place in set.mm
as well: if we
define extensional relation based on the common property in extid 34422,
extep 34389 and extssr 34599, then "extrelssr" " |- ExtRel
_S " is a theorem
along with "extrelep" " |- ExtRel _E " and
"extrelid" " |- ExtRel _I ".
(Contributed by Peter Mazsa, 25-Jul-2019.) |