Description: Define the reflexive relation predicate. (Read: R is a reflexive
relation.) This is a surprising definition, see the comment of
dfrefrel3 . Alternate definitions are dfrefrel2 and dfrefrel3 .
For sets, being an element of the class of reflexive relations
( df-refrels ) is equivalent to satisfying the reflexive relation
predicate, that is ( R e. RefRels <-> RefRel R ) when R is a set,
see elrefrelsrel . (Contributed by Peter Mazsa, 16-Jul-2021)