First order expression for functional dependency
Apparently, we must project away variable z from ternary relation Q, which is done via existential quantifier:

∀y1∀y2∀x:(∃z:Q(x1,y,z))∧(∃z:Q(x2,y,z))⟹x1=x2.

This is equivalent to standard textbook FD definition:

∀y1∀y2∀x∀z1∀z2:Q(x1,y,z1)∧Q(x2,y,z2)⟹x1=x2.