Is the variant direct image mathematically significant? Preimages have the property that for an arbitrary function $f : X \rightarrow Y$ and all $B \subseteq Y$ it holds that $$f^{-1}(B^c)=[f^{-1}(B)]^c.$$
However, the analogous statement for direct images is false. Thus, we have two definitions of direct image; the usual one, and a variant. $$f_*(A) = \{b \mid \exists a \in X : a \in A \,\wedge\, f(a)=b\}$$
$$f_\diamond(A) = \{b \mid \forall a \in X : a \in A \,\vee\, f(a) \neq b\}$$
Now I think (though I have not proved it) that, for all functions $f$, it holds that $f_* = f_\diamond$ iff $f$ is an injection bijection. Note also that, under these definitions, we have $$f_*(A^c) = [f_\diamond(A)]^c, \quad f_\diamond(A^c)=[f_*(A)]^c.$$
Here's another observation. If $X$ and $Y$ are topological spaces, then we have that $f_*$ preserves openness iff $f_\diamond$ preserves closedness, and vice versa.
Okay, but does $f_\diamond$ have any real mathematical significance? Like, does it show up naturally in any interesting theorems etc.? If so, what's the standard terminology/notation, and where can I learn more?

Addendum. Two related maps are $f_\cap(A) := f_*(A) \cap f_\diamond(A)$ and $f_\cup(A) := f_*(A) \cup f_\diamond(A).$ If anyone knows where I can learn more, please leave a comment! Note that all four concepts coincide in the case of bijections.
 A: The variant direct image is universal quantification. So if you think universal quantification is significant... 
To explain, let $X, Y$ be sets and let $f : X \times Y \to Y$ be the projection onto the second coordinate. If $\varphi(x, y)$ is any proposition involving variables $x \in X, y \in Y$, then it cuts out a subset of $X \times Y$ (namely the subset for which $\varphi(x, y)$ is true). The corresponding direct and variant direct image subsets in $Y$ are precisely the subsets of $Y$ cut out by the existentially and universally quantified statements $\exists x : \varphi(x, y)$ and $\forall x : \varphi(x, y)$ respectively. 

Much more generally, let $F : C \to C'$ be a functor between two categories and let $D$ be another category. Then $F$ induces a functor $D^{C'} \to D^C$ between functor categories. A left adjoint to this functor, if it exists, is called left Kan extension along $F$, and a right adjoint is called right Kan extension. 
Now let $C, C'$ be sets regarded as discrete categories (categories with only identity morphisms), and let $D = \{ 0 \to 1 \}$ be the category with two objects $0, 1$ and a single non-identity morphism $0 \to 1$. $D$ is a poset, and so are the functor categories $D^C, D^{C'}$, which are naturally identified with the poset of subsets of $C, C'$ under inclusion. If $F : C \to C'$ is a functor (so just a map of sets), the induced functor $D^{C'} \to D^C$ is the usual preimage functor, the usual direct image is the left Kan extension along $F$, and the variant direct image functor is the right Kan extension along $F$. 
Left and right Kan extension are ubiquitous in mathematics; Mac Lane famously said that they subsume all the other fundamental concepts in category theory. So it is a little hard to give examples because there are so many. This example is the simplest example I know. 
