| Description: Define the class of
converse reflexive relations. This is practically
dfcnvrefrels2 37398 (which uses the traditional subclass
relation ⊆) :
we use converse subset relation (brcnvssr 37376) here to ensure the
comparability to the definitions of the classes of all reflexive
(df-ref 23009), symmetric (df-syms 37412) and transitive (df-trs 37442) sets.
We use this concept to define functions (df-funsALTV 37551, df-funALTV 37552)
and disjoints (df-disjs 37574, df-disjALTV 37575).
For sets, being an element of the class of converse reflexive relations is
equivalent to satisfying the converse reflexive relation predicate, see
elcnvrefrelsrel 37406. Alternate definitions are dfcnvrefrels2 37398 and
dfcnvrefrels3 37399. (Contributed by Peter Mazsa,
7-Jul-2019.) |
