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	$$⊢\mathrm{RefRels}=\mathrm{Refs}\cap \mathrm{Rels}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crefrels	$$class\mathrm{RefRels}$$
1		crefs	$$class\mathrm{Refs}$$
2		crels	$$class\mathrm{Rels}$$
3	1 2	cin	$$class\left(\mathrm{Refs}\cap \mathrm{Rels}\right)$$
4	0 3	wceq	$$wff\mathrm{RefRels}=\mathrm{Refs}\cap \mathrm{Rels}$$