What does $\text{dom}(\Gamma)$ mean in the context of an inference rule?
There are various ways to define contexts in type theories. In this style, we assume there is some infinite set of variable names $V$ and define the context $\Gamma : V \rightharpoonup S$ as a partial function from the set of variable names to the set of types. $\mathrm{dom}(\Gamma)$ is then the subset of $V$ on which $\Gamma$ is defined, i.e. the variables in the context $\Gamma$. To require that $x \notin \mathrm{dom}(\Gamma)$ is asking for $x$ to be a fresh variable for the context $\Gamma$.