Metamath Proof Explorer


Definition df-br

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 R often denotes a relation such as " < " that compares two classes A and B , which might be numbers such as 1 and 2 (see df-ltxr for the specific definition of < ). As a wff, relations are true or false. For example, ( R = { <. 2 , 6 >. , <. 3 , 9 >. } -> 3 R 9 ) ( ex-br ). Often class R meets the Rel criteria to be defined in df-rel , and in particular R may be a function (see df-fun ). This definition of relations is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e., are not sets). On the other hand, we often find uses for this definition when R is a proper class (see for example iprc ). (Contributed by NM, 31-Dec-1993)

Ref Expression
Assertion df-br
|- ( A R B <-> <. A , B >. e. R )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cR
 |-  R
2 cB
 |-  B
3 0 2 1 wbr
 |-  A R B
4 0 2 cop
 |-  <. A , B >.
5 4 1 wcel
 |-  <. A , B >. e. R
6 3 5 wb
 |-  ( A R B <-> <. A , B >. e. R )