Definition of the value of a function in Enderton's Elements of Set-Theory In chapter 3 of his book Elements of Set Theory, Enderton defines the value of a funtion $F$ at a point $x$ in its domain $\text{dom} \, F$ to be the unique $y$ such that $\langle x,y \rangle \in F$, and denotes it by $F(x)$. Then, he explicitly resolves to use this notation only when $F$ is a function and $x \in \text{dom} \, F$.
Now consider the following problem (exercise 12 of the same chapter):


  
*Assume that $f$ and $g$ are functions and show that $$ f \subseteq g \iff  \text{dom} \, f \subseteq \text{dom} \, g \ \& \ (\forall x \in \text{dom}\,f) f(x) = g(x)$$
  

I'm having trouble going from the right to the left-hand side. It is intuitively clear to me that the implication is true. However, when trying to formalize my intuition, I get stuck. In particular, when trying to translate the statement $$(\forall x \in \text{dom}\,f) f(x) = g(x)$$ to a well formed formula (wff), I don't know how to handle the fact that if $x$ is not in $\text{dom}\,g$, then the expression $g(x)$ is meaningless (according to the notational convention stated above). 
I am aware that if the other right-hand side condition, $\text{dom} \, f \subseteq \text{dom} \, g$, is true, then $g(x)$ will always be meaningful. However, this doesn't seem to be of any help in obtaining a wff for  the previous expression, which should be meaningful independently of any conjuncts we might attach to it. 
I attempted a few different interpretations, which I later fully translated to wffs:


*

*$\forall x [x \in \text{dom}\,f \implies \forall y \forall z (\langle x,y \rangle \in f \& \langle x,z \rangle \in g \implies y=z)]$ 

*$\forall x [x \in \text{dom}\,f \implies (\text{$f$ and $g$ are functions defined over x} \implies \forall y \forall z (\langle x,y \rangle \in f \& \langle x,z \rangle \in g \implies y=z))]$ 

*$\forall x [x \in \text{dom}\,f \implies (\text{$f$ and $g$ are functions defined over x} \implies \exists y (\langle x,y \rangle \in f \& \langle x,y \rangle \in g))]$ 
They all seem to be sufficient conditions for $f \subseteq g$, because they guarantee, together with the other premises, the equality of $f(x)$ and $g(x)$ for every $x \in \text{dom} \, f$. However, they are clearly not equivalent. Is there a true or real ambiguity in the statement of the problem or am I missing something?
 A: In a statement like you have:(1) (for every x$\in$domain(f)) f(x)=g(x) ; should be considered as false in case "g(x)" is undefined or meaningless . So assuming the right side of 12 is true ,means the statement f(x)=g(x) in 12 is an abbreviation   for f(x)=y and (x,y)$\in$g . This probably gets you through this problem because of the quantifier ,for every x in domain(f) but the term "f(x)" is not always defined either . What you really need to do is define f(x) when x is not in   domain(f), to be something not in the range of f,that is not a value of f . If you were using a set theory with classes where sets are classes that are elements of other classes (like Kelly- Moore ) then you can just take f(x)=U (the class of all sets ) for any f and any x not in domain(f) . 
  In set theory without classes I don't think  there is one U that would work for all functions .  
There is another point I wish to make . When you make a definition of a term you enlarge the language of both terms and wff's . For the new term f(x) you do it by a defining axiom  : f(x) = y $\iff$ (x,y)$\in$f . You are required to show that y is unique (ok since f is a function) but f(x) or y is a set (meaningful)only when x$\in$domain(f) ;otherwise the term f(x) denotes nothing ,has no denotation .Nevertheless f(x) = (some other term ) is a well formed formula of the extended language ;which will always be equivalent to some formula of the original language before definitions .
 So here with y=f(x) (x ,f(x)) $\in$domain(f) we have , f(x)=g(x) $\iff$g(x)=f(x)$\iff$(x,f(x))$\in$g proving that f$\subseteq$g .
So your worry never comes up , the defining equivalence includes the fact that  f(x) =g(x) and f(x) is a set (has a denotation ) then so does g(x) .Regards  
