Definition df-rels 39147

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

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 39149. 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 39297), 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 39147 (see df-refrels 39298 and the resulting dfrefrels2 39300 and dfrefrels3 39301).

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

Assertion

Ref	Expression
df-rels	⊢ Rels = 𝒫 (V × V)

Detailed syntax breakdown of Definition df-rels

Step	Hyp	Ref	Expression
1		crels 38892	. 2 class Rels
2		cvv 3457	. . . 4 class V
3	2, 2	cxp 5661	. . 3 class (V × V)
4	3	cpw 4564	. 2 class 𝒫 (V × V)
5	1, 4	wceq 1570	1 wff Rels = 𝒫 (V × V)

This definition is used by:  elrels2  39148