Definition df-ssr

Description: Define the subsets class or the class of subset relations. Similar to definitions of epsilon relation ( df-eprel ) and identity relation ( df-id ) classes. Subset relation class and Scott Fenton's subset class df-sset are the same: _S = SSet (compare dfssr2 with df-sset ), the only reason we do not use dfssr2 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 ) are the same, that is, ( AS B <-> A C B ) when B is a set, see brssr . Yet in general we use the subclass relation A C_ B both for classes and for sets, see the comment of df-ss . The only exception (aside from directly investigating the class _S e.g. in relssr or in extssr ) is when we have a specific purpose with its usage, like in case of df-refs versus df-cnvrefs , 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 , extep and extssr , then "extrelssr" " |- ExtRel _S " is a theorem along with "extrelep" " |- ExtRel _E " and "extrelid" " |- ExtRel _I " . (Contributed by Peter Mazsa, 25-Jul-2019)

	Ref	Expression
Assertion	df-ssr	|- _S = { <. x , y >. | x C_ y }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cssr	|- _S
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4	2	cv	|- y
5	3 4	wss	|- x C_ y
6	5 1 2	copab	|- { <. x , y >. | x C_ y }
7	0 6	wceq	|- _S = { <. x , y >. | x C_ y }