Definition df-refrels

Description: Define the class of reflexive relations. This is practically dfrefrels2 (which reveals that RefRels can not include proper classes like _I as is elements, see comments of dfrefrels2 ).

Another alternative definition is dfrefrels3 . The element of this class and the reflexive relation predicate ( df-refrel ) are the same, that is, ( R e. RefRels <-> RefRel R ) when A is a set, see elrefrelsrel .

This definition is similar to the definitions of the classes of symmetric ( df-symrels ) and transitive ( df-trrels ) relations. (Contributed by Peter Mazsa, 7-Jul-2019)

	Ref	Expression
Assertion	df-refrels	|- RefRels = ( Refs i^i Rels )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crefrels	|- RefRels
1		crefs	|- Refs
2		crels	|- Rels
3	1 2	cin	|- ( Refs i^i Rels )
4	0 3	wceq	|- RefRels = ( Refs i^i Rels )