| Description: Define the class of
converse reflexive relations. This is practically
dfcnvrefrels2 39460 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 39438) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 23785), symmetric (df-syms 39474) and transitive (df-trs 39508) sets.
We use this concept to define functions (df-funsALTV 39618, df-funALTV 39619)
and disjoints (df-disjs 39641, df-disjALTV 39642).
For sets, being an element of the class of converse reflexive relations is
equivalent to satisfying the converse reflexive relation predicate, see
elcnvrefrelsrel 39468. Alternate definitions are dfcnvrefrels2 39460 and
dfcnvrefrels3 39461. (Contributed by Peter Mazsa,
7-Jul-2019.) |
