**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) |

0. Set of symbols

1. Alphabet

2. Deduction system

3. Theory

4. Zermelo-Fraenkel set theory

5. Set

6. Binary cartesian set product

1. Alphabet

2. Deduction system

3. Theory

4. Zermelo-Fraenkel set theory

5. Set

6. Binary cartesian set product

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

» 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