¹Here x : u →v means that x is an appropriate set of ordered pairs, according to the usual way of encoding functions in set theory.