Mathbox for Peter Mazsa < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ssr Structured version   Visualization version   GIF version

Definition df-ssr 35857
 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.)
Assertion
Ref Expression
df-ssr S = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-ssr
StepHypRef Expression
1 cssr 35575 . 2 class S
2 vx . . . . 5 setvar 𝑥
32cv 1537 . . . 4 class 𝑥
4 vy . . . . 5 setvar 𝑦
54cv 1537 . . . 4 class 𝑦
63, 5wss 3908 . . 3 wff 𝑥𝑦
76, 2, 4copab 5104 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
81, 7wceq 1538 1 wff S = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}
 Colors of variables: wff setvar class This definition is referenced by:  dfssr2  35858  relssr  35859  brssr  35860
 Copyright terms: Public domain W3C validator