How to phrase a proof of a function from a set A to a set B Here is a problem:
Let $f \subseteq A \times B$ be a function. In many situations you may want to restrict the domain of $f$ or expand its range. If $C \subseteq A$ then define the restriction of $f$ to $C$ as 
$$f|C = (C \times B)\cap f$$
Prove that $f|C $ is  a function from $C$ to $B$.
I understand the idea and concept to solve it but I have some difficult proving it. Here is my proof:
By the definition of Cartesian product of sets, $C \times B = \{(c,b)|c \in C \mbox{ and } b \in B \}$.
Also, by the definition of a function from a set to another set,  $f \subseteq A \times B$ is a function such that for each element $a \in A$ there is a unique element $(a, b) \in f$.
Since $c \in C$ and $C \subseteq A$, $c \in A$.
Then, we know that for $(d,e) \in (C \times B) \cap f$, for each element $d \in A$ there is a unique element $(d,e) \in f|C$.
Also, since $f$ covers all the unique cases of $a \in A$ and $c \in C \subseteq A$, $f|C$ covers all the unique $c \in C$.
Thus, we can conclude that $f|C $ is  a function from $C$ to $B$.
Hope some one can help me to improve my proof.
Thank you!
 A: The wording is a bit confuse, but your argument is sound. 
Let $c \in C$. Then $c \in A$ and, since $f \colon A \to B$ is a function, there is a unique $b \in B$ such that $(c,b) \in f$ and furthermore $(c,b) \in f \restriction C$. Combined with the obvious fact that $f \restriction C \subseteq C \times B$, this proves that $f \restriction C \colon C \to B$    is indeed a function.
A: The idea is essentially correct, but the write-up should be better.
Let $f|C := (C \times B) \cap f$.
This should be a function from $C$ to $B$.
So it should satisfy $f|C \subseteq C \times B$, which is clear (as $X \cap Y \subseteq X$ for all sets $X,Y$).
Pick $c \in C$. Then $c \in A$, as $C \subseteq A$.
As $f$ is a function from $A$ to $B$, there exists $b \in B$ with $(c,b) \in f$, and as $(c,b) \in C \times B$ by definition, $(c,b) \in f|C$. 
And as to unicity: if $(c,b_1), (c,b_2)$ are both in $f|C$, then in particular $(c,b_1), (c,b_2) \in f$, so by unicity of images in $f$, $b_1 = b_2$, and we are done.
A: I think it would be more elegant to prove it without reference to elements.  How about this informal proof:  for every set $X$, we have $X\cap f\subseteq f $.  Since $f $ is a function, and $f\mid C\subseteq f $, and a subset of a function is a function, $f\mid C $ is a function.  Since $dom f| C\subseteq C$ and $codom f|C, = B$, it follows that $f $ is a function from $C $ to $B $.
