The image of a function $f:A\to B$ isThe function is surjective, or onto, exactly when every $b\in B$ equals $f(a)$ for at least one $a\in A$, equivalently $f(A)=B$. It is injective, or one-to-one, exactly whenThus surjectivity concerns whether the entire codomain is reached; injectivity concerns whether distinct inputs have distinct outputs.

The premise limits every possible existential witness to the objects named by $c_0,c_1$; it does not assert that these constants name distinct objects. Instantiate it at a fresh witness $v$, then apply disjunction elimination. In the first case equality elimination rule transfers $R(v)$ to $R(c_0)$; in the second it transfers $R(v)$ to $R(c_1)$, contradicting the assumed negation. The full natural deduction derivation isThe sibling case subproofs end before the witness subproof closes. At line 13, $v$ is absent from $R(c_0)$ and from all surrounding assumptions, so no witness escape occurs. The final two applications of implication introduction giveThe logical falsity elimination rule is needed to complete the contradictory second case with the same conclusion as the first case.

Use a fresh existential witness $v$. Within the assumption of the forbidden universal quantification, eliminate the original existential quantification to obtain logical falsity:The witness $v$ appears neither in the exported conclusion $\perp$ at line 6 nor in the other undischarged assumptions. The existential quantifier elimination rule is therefore valid, and