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 ∩ Rels )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crefrels	⊢ RefRels
1		crefs	⊢ Refs
2		crels	⊢ Rels
3	1 2	cin	⊢ ( Refs ∩ Rels )
4	0 3	wceq	⊢ RefRels = ( Refs ∩ Rels )