| Description: Define the class of
converse reflexive relations. This is practically
dfcnvrefrels2 36686 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 36666) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 22701), symmetric (df-syms 36698) and transitive (df-trs 36728) sets.
We use this concept to define functions (df-funsALTV 36834, df-funALTV 36835)
and disjoints (df-disjs 36857, df-disjALTV 36858).
For sets, being an element of the class of converse reflexive relations is
equivalent to satisfying the converse reflexive relation predicate, see
elcnvrefrelsrel 36692. Alternate definitions are dfcnvrefrels2 36686 and
dfcnvrefrels3 36687. (Contributed by Peter Mazsa,
7-Jul-2019.) |
