Notation for expressing a straight chain of $n \choose 2$ identity statements

Question

Given the glossary $Dx$: $x$ is a dog, we can make the following translations:

• "there is at least one dog" - $\exists x Dx$.
• "there are at least two dogs" - $\exists x \exists y (Dx \land Dy \land x \ne y)$.
• "there are at least three dogs" - $\exists x \exists y \exists z (Dx \land Dy \land Dz \land x \ne y \land x \ne z \land y \ne z)$.

In general, if we want to say that there are at least $n$ dogs, we need $n$ variables, $n$ existential quantifiers (one for each variable) prefixed to a conjunction of $n$ atomic formulas of the form $D\underline{x}$ and $n \choose 2$ identity statements (one for each unordered pairing of the $n$ variables). I understand this as saying "you can choose at least $n$ distinct objects that have the property of being a dog."

• "there is at most one dog" - $\forall x \forall y ((Dx \land Dy) \implies x = y)$.
• "there are at most two dogs" - $\forall x \forall y \forall z ((Dx \land Dy \land Dz) \implies x = y \lor x = z \lor y = z)$.
• "there are at most three dogs" - $\forall x \forall y \forall z \forall w ((Dx \land Dy \land Dz \land Dw) \implies x = y \lor x = z \lor x = w \lor y = z \lor y = w \lor z = w)$.

In general, if we want to say that there are at most $n$ dogs, we need $n+1$ variables, $n+1$ universal quantifiers (one for each variable) prefixed to a conditional. The antecedent of this conditional is a conjunction of $n+1$ atomic formulas of the form $D\underline{x}$. The consequent of this conditional is a disjunction of $n + 1 \choose 2$ identity statements (one for each unordered pairing of the $n+1$ variables). I understand this as saying "for any $n+1$ objects you choose, if they all have the property of being a dog, then at least two of those objects must be the same objec."

But I was wondering if there was a way to express this pattern more visually using symbols rather than words? Something like $\exists x_1 \exists x_2 ... \exists x_n (Dx_1 \land Dx_2 \land ... \land Dx_n \land ?)$, but I'm not sure how to express the unordered pairs part (hence the question mark).