Description: Define the class of
converse reflexive relations. This is practically
dfcnvrefrels2 36980 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 36958) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 22854), symmetric (df-syms 36994) and transitive (df-trs 37024) sets.
We use this concept to define functions (df-funsALTV 37133, df-funALTV 37134)
and disjoints (df-disjs 37156, df-disjALTV 37157).
For sets, being an element of the class of converse reflexive relations is
equivalent to satisfying the converse reflexive relation predicate, see
elcnvrefrelsrel 36988. Alternate definitions are dfcnvrefrels2 36980 and
dfcnvrefrels3 36981. (Contributed by Peter Mazsa,
7-Jul-2019.) |