 Solution

The equality predicate on $A$ is interpreted by the diagonal monomorphism ${\Delta }_A:A\hookrightarrow A\times A$. The antecedent equality of the two $f$-values is the kernel pair $A{\times }_{B}A\hookrightarrow A\times A$. Semantic validity of the implication says that the kernel-pair subobject is contained in the diagonal; the reverse containment always holds. Hence the sequent is valid exactly whenIf $f$ is monic, this equality is its cancellation property expressed by the pullback. Conversely, if $fr=fs$ for $r,s:X\to A$, then $(r,s)$ factors through this kernel pair and therefore through the diagonal, giving $r=s$. Thus the sequent holds exactly when the map is a monomorphism. This argument uses generalized arrows from arbitrary $X$, not a claim that global elements detect maps.