Let $\phi: F\rightarrow G$ be a relation and $id_F$ be the identity relation on $F$. Then $\phi\circ id_F = \phi$ .
Attempted proof: $$\phi\ \circ id_F = \{(f,g)\in F\times G: \exists f_2\in F((f_1,f_2)\in id_F \ and \ (f_2, g)\in \phi)\}$$ $$= \{(f,g)\in F\times G: \exists f_2\in F((f_2, g)\in \phi)\}$$ $$= \{(f,g)\in F\times G: (f, g)\in \phi\}$$ $$= \phi \ . $$
In line 1, do we read "...such that there exists $f_2$ in $F$ such that for some $f_1$ in $F$..."?
And can "$(f_1,f_2)\in id_F$" be "eliminated" by the observation that it holds for all members of $F$, and so existentially quantifying it is useless?
Finally, is there any elementary reference for such quantifier elimination?
Edit: I should clarify the reference request; I'm sure I could find something by googling, but would I search for "quantifier elimination" or "quantifiers in set builder notation", etc. to learn about these kinds of problems?