Description: Define the relations class. Proper class relations (like _I , see
reli ) are not elements of it. The element of this class and the
relation predicate are the same when R is a set (see elrelsrel ).

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 .
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 ), 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 (see
df-refrels and the resulting dfrefrels2 and dfrefrels3 ).

3. Finally, in order to be able to work with proper classes (like
iprc ) as well, we define the predicate of the relation (see
df-refrel ) so that it is true for the relevant proper classes (see
refrelid ), and that the element of the class of the required relations
(e.g. elrefrels3 ) and this predicate are the same in case of sets (see
elrefrelsrel ). (Contributed by Peter Mazsa, 13-Jun-2018)