Binary Operations on a Set

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $a$ be a set.

¶ A binary operation on $a$ is a function from the Cartesian product $a\times a$ to $a$.

¶ Let $\ast$ be a binary operation on $a$ and $u,v\in a$. Then $u\ast v$ denotes the value $\ast((u,v))$ of $\ast$ at the ordered pair $(u,v)$. This value exists because $(u,v)\in a\times a$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership and $a\times a=\operatorname{dom}\ast$ by Functions, Values of a Function, and Functions from One Class to Another §map; and it lies in $a$, since it lies in the range $\operatorname{ran}\ast$ by Relations, Domain, Range, Inverse and Composition §range and $\operatorname{ran}\ast\subseteq a$ by Functions, Values of a Function, and Functions from One Class to Another §map. By Functions, Values of a Function, and Functions from One Class to Another §value, $u\ast v$ is the unique set $z$ with $((u,v),z)\in\ast$, so it is a defined set symbol.