Description: If two classes are related by a restricted binary relation, then the first
class is an element of the restricting class. See also brres and
brrelex1 .

Remark: there are many pairs like bj-opelresdm / bj-brresdm , where
one uses membership of ordered pairs and the other, related classes (for
instance, bj-opelresdm / brrelex12 or the opelopabg / brabg family). They are straightforwardly equivalent by df-br . The latter
is indeed a very direct definition, introducing a "shorthand", and barely
necessary, were it not for the frequency of the expression A R B .
Therefore, in the spirit of "definitions are here to be used", most
theorems, apart from the most elementary ones, should only have the "br"
version, not the "opel" one. (Contributed by BJ, 25-Dec-2023)