| Description: Define the class of
converse reflexive relations. This is practically
dfcnvrefrels2 38888 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 38866) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 23466), symmetric (df-syms 38902) and transitive (df-trs 38936) sets.
We use this concept to define functions (df-funsALTV 39046, df-funALTV 39047)
and disjoints (df-disjs 39069, df-disjALTV 39070).
For sets, being an element of the class of converse reflexive relations is
equivalent to satisfying the converse reflexive relation predicate, see
elcnvrefrelsrel 38896. Alternate definitions are dfcnvrefrels2 38888 and
dfcnvrefrels3 38889. (Contributed by Peter Mazsa,
7-Jul-2019.) |
