| Description: Define the class of
converse reflexive relations. This is practically
dfcnvrefrels2 38004 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 37982) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 23427), symmetric (df-syms 38018) and transitive (df-trs 38048) sets.
We use this concept to define functions (df-funsALTV 38157, df-funALTV 38158)
and disjoints (df-disjs 38180, df-disjALTV 38181).
For sets, being an element of the class of converse reflexive relations is
equivalent to satisfying the converse reflexive relation predicate, see
elcnvrefrelsrel 38012. Alternate definitions are dfcnvrefrels2 38004 and
dfcnvrefrels3 38005. (Contributed by Peter Mazsa,
7-Jul-2019.) |
