Description: Define a general binary
relation. Note that the syntax is simply three
class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29
generalized to arbitrary classes. Class  often denotes a relation
such as " " that compares two classes  and  , which might
be numbers such as 
and  (see df-ltxr 9636 for the specific
definition of ). As a wff, relations are true or false. For
example,       
     (ex-br 25130).
Often class
meets the 
criteria to be defined in df-rel 4996,
and in particular may be a function (see df-fun 5580). This
definition of relations is well-defined, although not very meaningful,
when classes
and/or are proper
classes (i.e. are not sets).
On the other hand, we often find uses for this definition when is a
proper class (see for example iprc 6720). (Contributed by NM,
31-Dec-1993.) |
