Definition df-ssr 39205

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

Assertion

Ref	Expression
df-ssr	⊢ S = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊆ 𝑦}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-ssr

Step	Hyp	Ref	Expression
1		cssr 38813	. 2 class S
2		vx	. . . . 5 setvar 𝑥
3	2	cv 1569	. . . 4 class 𝑥
4		vy	. . . . 5 setvar 𝑦
5	4	cv 1569	. . . 4 class 𝑦
6	3, 5	wss 3906	. . 3 wff 𝑥 ⊆ 𝑦
7	6, 2, 4	copab 5174	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊆ 𝑦}
8	1, 7	wceq 1570	1 wff S = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊆ 𝑦}

This definition is referenced by:  dfssr2  39206  relssr  39207  brssr  39208