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	$$⊢ARB\leftrightarrow ⟨A,B⟩\in R$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cR	$$classR$$
2		cB	$$classB$$
3	0 2 1	wbr	$$wffARB$$
4	0 2	cop	$$class⟨A,B⟩$$
5	4 1	wcel	$$wff⟨A,B⟩\in R$$
6	3 5	wb	$$wff\left(ARB\leftrightarrow ⟨A,B⟩\in R\right)$$