Definition df-refrels 34748

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

Another alternative definition is dfrefrels3 34751. The element of this class and the reflexive relation predicate (df-refrel 34749) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, cf. elrefrelsrel 34756.

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

Assertion

Ref	Expression
df-refrels	⊢ RefRels = ( Refs ∩ Rels )

Detailed syntax breakdown of Definition df-refrels

Step	Hyp	Ref	Expression
1		crefrels 34467	. 2 class RefRels
2		crefs 34466	. . 3 class Refs
3		crels 34464	. . 3 class Rels
4	2, 3	cin 3767	. 2 class ( Refs ∩ Rels )
5	1, 4	wceq 1653	1 wff RefRels = ( Refs ∩ Rels )

This definition is referenced by:  dfrefrels2  34750