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