Proof of Values of a Map between Classes, and Distances in a Metric Space

Every element of a class is a set by Classes, Membership, Sets and Proper Classes (i); in particular $a$, and below $x$ and $y$, are sets. By Functions, Values of a Function, and Functions from One Class to Another (iii), $F$ is a function with $\operatorname{dom}F=A$, so by Functions, Values of a Function, and Functions from One Class to Another (ii) $F(a)$ is the unique set $v$ with $(a,v)\in F$. In particular $F(a)$ is a set, which is (i), and $(a,F(a))\in F$, which is (ii).

By Relations, Domain, Range, Inverse and Composition (iii) and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), applied to the set $F(a)$, $F(a)\in\operatorname{ran}F$ holds if and only if there is a set $u$ with $(u,F(a))\in F$; by (ii) the set $u=a$ is one, so $F(a)\in\operatorname{ran}F$. By Functions, Values of a Function, and Functions from One Class to Another (iii), $\operatorname{ran}F\subseteq B$, so $F(a)\in B$ by Subclasses and Subsets (i). This is (iii).

For (iv): by Metric Space (vi) and the standing hypothesis of Metric Space, $d$ is a map $d:M\times M\to\mathbb{R}$, a map in the sense of Functions, Values of a Function, and Functions from One Class to Another (iii) as fixed by Sets and Maps: Ordinary Notation (v). Since $x$ and $y$ are sets, $(x,y)\in M\times M$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i). Applying (iii) to the map $d$ from the class $M\times M$ to the class $\mathbb{R}$ at the element $(x,y)$ gives $d((x,y))\in\mathbb{R}$, which by Sets and Maps: Ordinary Notation (v) is $d(x,y)\in\mathbb{R}$.