This is a very useless definition, which "abbreviates" as . What this display hides, though, is that the first expression, even though it has a shorter constant string, is actually much more complicated in its parse tree: it is parsed as (wi (wceq (cv vx) (cv vy)) wph), while the version is parsed as (wcdeq vx vy wph). It also allows us to give a name to the specific ternary operation .
This is all used as part of a metatheorem: we want to say that and are provable, for any expressions or in the language. The proof is by induction, so the base case is each of the primitives, which is why you will see a theorem for each of the set.mm primitive operations.
The metatheorem comes with a disjoint variables assumption: every variable in is assumed disjoint from except itself. For such a proof by induction, we must consider each of the possible forms of . If it is a variable other than , then we have or , which is provable by cdeqth and reflexivity. Since we are only working with class and wff expressions, it can't be itself in set.mm, but if it was we'd have to also prove (where set equality is being used on the right).
Otherwise, it is a primitive operation applied to smaller expressions. In these cases, for each setvar variable parameter to the operation, we must consider if it is equal to or not, which yields 2^n proof obligations. Luckily, all primitive operations in set.mm have either zero or one setvar variable, so we only need to prove one statement for the non-set constructors (like implication) and two for the constructors taking a set (the universal quantifier and the class builder).
In each of the primitive proofs, we are allowed to assume that is disjoint from and vice versa, because this is maintained through the induction. This is how we satisfy the disjoint variable conditions of cdeqab1 and cdeqab.