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 ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cR 𝑅
2 cB 𝐵
3 0 2 1 wbr 𝐴 𝑅 𝐵
4 0 2 cop 𝐴 , 𝐵
5 4 1 wcel 𝐴 , 𝐵 ⟩ ∈ 𝑅
6 3 5 wb ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )