 Function extensionality

For two mathematical functions $f,g:A\to B$ with the same domain and codomain, equality is equivalent to equality of their values at every argument. In the set-theoretic representation, their graphs of functions then contain exactly the same ordered pairs. This permits a function identity to be proved by fixing an arbitrary argument and proving the resulting value equality.