Let $V$ be a set and let $R\subseteq V\times V$ be a binary relation $R$ is called extensional if all elements of $x\in V$ are uniquely determined by ordered pairs $(z,x)\in R,$ formally
$$\{z\in V\mid zRx\}=\{z\in V\mid zRy\} \Rightarrow x=y,$$
or, by contraposition,
$$x\neq y \Rightarrow \{z\in V\mid zRx\}\neq \{z\in V\mid zRy\} .$$
Explanations: 1
Explanations: 1
Motivations: 2
Proofs: 3 4 5 6 7
Propositions: 8 9 10
Theorems: 11