Existential quantification over a finitely named domain ($\exists xQ(x)⟷Q(c_1)\vee \cdots \vee Q(c_n)$)

Assume $\forall x(x=c_1\vee \cdots \vee x=c_n)$ with $n\ge 1$. For the forward implication, open a fresh existential witness, instantiate domain exhaustiveness at it, and split into the equality cases. The equality elimination rule transfers its predicate to the corresponding constant, which supplies the required disjunct. Closing the witness scope is legal because the result contains only the named constants. Conversely each named instance gives the existential by the existential quantifier introduction rule, and cases combine those derivations. The constants need not denote distinct objects. A negated named instance can eliminate one case through contradiction and logical falsity elimination rule.