**Description: **Define the subsets class
or the class of subset relations. Similar to
definitions of epsilon relation (df-eprel 5442) and identity relation
(df-id 5437) classes. Subset relation class and Scott
Fenton's subset
class df-sset 33391 are the same: S = SSet (compare dfssr2 35858 with
df-sset 33391), the only reason we do not use dfssr2 35858 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 subsets and the subclass
relationship (df-ss 3925) are the same, that is,
(𝐴
S 𝐵 ↔ 𝐴 ⊆ 𝐵) when 𝐵 is a set, see brssr 35860. Yet in
general we use the subclass relation 𝐴 ⊆ 𝐵 both for classes and for
sets, see the comment of df-ss 3925. The only exception (aside from
directly investigating the class S e.g. in relssr 35859 or in
extssr 35868) is when we have a specific purpose with its
usage, like in
case of df-refs 35869 versus df-cnvrefs 35882, 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 35687,
extep 35659 and extssr 35868, then "extrelssr" " |- ExtRel
S " is a
theorem along with "extrelep" " |- ExtRel E " and "extrelid" " |-
ExtRel I " . (Contributed by Peter Mazsa,
25-Jul-2019.) |