I'm working through Enderton's book on set theory. In chapter 3, there are a series of exercises regarding functions. For instance
- Prove that if $F$ and $G$ are functions, $dom(F) = dom(G)$, and $F(x) = G(x)$ for all $x$ in the common domain, then $F = G$.
- Assume that $F$ and $G$ are functions. Show that $F \subseteq G$ if and only if $dom(F) \subseteq dom(G)$ and $F(x) = G(x)$ for all $x \in dom(F)$.
If I think about the statements, I come up with the following "sketches:"
- Suppose $(x,F(x)) \in F$. Then $x \in dom(F)$. Since $dom(F) = dom(G)$, $x \in dom(G)$ and $(x,G(x)) \in G$. Since $G(x) = F(x)$ for all $x$ in the common domain, $(x,F(x)) \in G$. The other direction is similar.
- Assume $F$ and $G$ are functions. Then $F \subseteq G$ iff $(x,y) \in F$ implies $(x,y) \in G$. Hence, $x \in dom(F)$ implies $x \in dom(G)$ and $dom(F) \subseteq dom(G)$. Similarly, $(x,y) \in F$ implies $(x,y) \in G$ iff $F(x) = G(x)$ for all $x \in dom(F)$ since $F$ and $G$ are functions and $y$ is uniquely determined by $x$.
But these are not formal proofs. I am having trouble in these exercises with formalizing the idea that I want to express. Hence, the question (request) is for an example of a formalization, so that I can see the appropriate style and level of detail involved.