# 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}⟩\in {R}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 cR ${class}{R}$
2 cB ${class}{B}$
3 0 2 1 wbr ${wff}{A}{R}{B}$
4 0 2 cop ${class}⟨{A},{B}⟩$
5 4 1 wcel ${wff}⟨{A},{B}⟩\in {R}$
6 3 5 wb ${wff}\left({A}{R}{B}↔⟨{A},{B}⟩\in {R}\right)$