Description: For sets, being an element of the class of converse reflexive relations ( df-cnvrefrels ) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021)