Past exam of the mathematics course of the University of Cambridge / 2010 / iii / Paper 75 / 7 / ii

In a regular category, interpret existential quantification by the image of the appropriate projection. The relation $f(x)=y$ is the graph of $f$, isomorphic to $A$; its projection to $B$ is $f$ itself. Thus the subobject interpreting the existential predicate is $\mathrm{im}(f)\hookrightarrow B$. Semantic validity of the sequent means this image is the whole object.

The regular image factorization writes $f=me$ with $e$ a regular epimorphism and $m$ its monic image inclusion. Its image is all of $B$ exactly when $m$ is invertible, equivalently when $f$ is itself a regular epimorphism. This is precisely the cover condition in a regular category.