| Description: Define the relations
class.  Proper class relations (like I, see
     reli 5836) are not elements of it.  The element of this
class and the
     relation predicate are the same when 𝑅 is a set (see elrelsrel 38488). 
     The class of relations is a great tool we can use when we define classes
     of different relations as nullary class constants as required by the 2.
     point in our Guidelines https://us.metamath.org/mpeuni/mathbox.html 38488.
     When we want to define a specific class of relations as a nullary class
     constant, the appropriate method is the following:
 
     1.  We define the specific nullary class constant for general sets (see
     e.g. df-refs 38511), then
 
     2. we get the required class of relations by the intersection of the class
     of general sets above with the class of relations df-rels 38486 (see
     df-refrels 38512 and the resulting dfrefrels2 38514 and dfrefrels3 38515).
 
     3.  Finally, in order to be able to work with proper classes (like
     iprc 7933) as well, we define the predicate of the
relation (see
     df-refrel 38513) so that it is true for the relevant proper
classes (see
     refrelid 38523), and that the element of the class of the
required relations
     (e.g. elrefrels3 38520) and this predicate are the same in case of
sets (see
     elrefrelsrel 38521).  (Contributed by Peter Mazsa,
13-Jun-2018.) |