0. Set of symbols
1. Alphabet
2. Deduction system
3. Theory
4. Zermelo-Fraenkel set theory
5. Set
6. Binary cartesian set product
Binary relation
Formulation 0
An D548: Ordered pair $(X \times Y, R)$ is a binary relation if and only if
(1) $X \times Y$ is a D191: Binary cartesian set product
(2) $R \subseteq X \times Y$ (D78: Subset)
Child definitions
» D4424: Binary endorelation
» D1104: Binary relation structure
» D857: Empty binary relation
» D362: Inverse binary relation
» D357: Left-unique binary relation
» D18: Map
» D4583: Maximal binary relation
» D4423: Relation class
» D358: Right-unique binary relation
» D5348: Set of binary relations
» D294: Symmetric binary relation