Two-sorted logic is not an "informal short-cut", it is actually a different way of setting up formal logic. In particular, the two different kinds of variables actually matter to the semantics.
So, if you set up Morse-Kelly set theory as a two-sorted theory, then a model is not just a set $M$ together with a relation $\in$ but rather a tuple $(M,S,C,\in)$ where $M$ is a set, $S$ and $C$ are subsets of $M$ (the sets and classes) whose union is $M$, and $\in$ is a binary relation on $M$. When we interpret formulas in such a structure, the set variables get interpreted as elements of $S$ and the class variables as elments of $C$. In other words, if $x$ is a set variable, then $M\models\forall x[\varphi(x)]$ is defined as $\forall a\in S, M\models \varphi(a)$, and similarly for class variables and existential quantifiers. Similarly, if you're studying proofs, then every variable has a sort and all the deduction rules need to respect these sorts, so for instance when you use universal instantiation you are only allowed to replace the quantified variable with another variable of the same sort. As a result, proofs will be sound with respect to this semantics.
Now a warning: the setup above is not quite the usual definition of multisorted logic. Usually in multisorted logic, the sets for different sorts are required to be disjoint (so $S$ and $C$ would be disjoint), and all the function and relation symbols must specify (as part of their "arity") the sorts of their inputs (and output, for functions). So for instance, to talk about something like modules over a ring, you would have a language with two sorts $R$ (the ring) and $M$ (the module), and for each of the different function symbols you would specify their input and output; for instance, there would be both an addition function $+_R$ which takes two inputs in $R$ and gives an output in $R$ and an addition function $+_M$ which takes two inputs in $M$ and gives an output in $M$, and there would be a scalar multiplication function $\cdot_M$ which takes an input in $R$ and an input in $M$ and gives an output in $M$. A model would then be a tuple $(X,R,M,+_R,+_M,\cdot_M,\dots)$ (there are a few more functions needed which I've omitted) where $R$ and $M$ are disjoint sets whose union is $X$, $+_R$ is a function $R\times R\to R$, $+_M$ is a function $M\times M\to M$, and so on. Moreover, in this language, not only does each variable have a type, but each term has a type: for instance, if $r$ and $s$ are $R$-variables, then $+_R(r,s)$ is an $R$-term, but $+_M(r,s)$ is not a well-formed term at all since we can't input $R$-variables into $+_M$.
This usual definition doesn't work so well for Morse-Kelly because we'd like to be able to talk about sets being equal to classes, and sets being elements of both sets and classes. To use disjoint types, in a model we would need to have, for each set, a "copy" of the set which is a class with the same elements but is not literally equal. We would also need to have two different element relations $\in_S$ and $\in_C$, where $\in_S$ is a relation between two sets and $\in_C$ is a relation between a set and a class. We couldn't actually talk about sets and classes being equal (since they never are!), and to say something like $\forall x \exists X (x = X)$ we would need to say that $x=X$ is actually just an abbreviation for $\forall y(y\in_S x\Leftrightarrow y\in_C X)$.