Jech 3rd Edition Section 12 page 162 Models of Set Theory Jech page 162 states : 
Let Form denote the set of all formulas of the language {$\in$}. As with any actual (metamathematical) natural number we can associate the corresponding element of N (i.e. the smallest inductive set), we can similarly associate with any given formula of set theory the corresponding element of the set Form. To make the distinction, if $\varphi$ is a formula, let $\ulcorner \varphi \urcorner    $ denote the corresponding element of Form.
If M is a set and E is a binary relation on M and if $a_1,..,a_n$ are elements of M, then
(12.16)$\hspace{2cm} \varphi^M{^,}^E(a_1,...,a_n)\leftrightarrow(M,E)\models\ulcorner \varphi \urcorner[a_1,...,a_n]$
as can be easily verified. Thus in the case when M is a set and $\varphi$ a particular (metamathematical) formula, we shall not make a distinction between the two meanings of the symbol $\models$. We note however that the left-hand side of (12.16) (relativization) is not defined for $\varphi$ $\in$ Form, and the right-hand side (satisfaction) is not defined if M is a proper class.
Would it be possible to ask two questions :
1) As Jech works in ZFC metatheory, is Form a set in the metatheory defined by a metamathematical ZFC formula with its variables ranging over the formulae $\varphi$ coded as metamathematical ZFC sets  $\ulcorner \varphi \urcorner$.
and
2) Why in (12.16) does $\ulcorner \varphi \urcorner$ appear on the right hand side, and not just $\varphi$, with (12.16) being a metamathematical ZFC formula, or is (12.16) actually a metamathematical ZFC formula thats using coded formula within the coded logic & model theory? (apologies this isnt too clear - hence the question - I tried to use https://mathoverflow.net/questions/23060/set-theory-and-model-theory/23077#23077). If anyone knows of a book that describes in detail how metamathematical ZFC can be used to code logic & model theory that would be good to know. 
 A: I'll answer your second question first: I don't really know of a book that discusses exactly what is going on in this case in depth. But the ideas of coding used here are the same as those in Godel's incompleteness theorem. Recall that $ZFC$ is formally a countable language. So that kind of coding makes sense. This can be done with PRA for example, which is much weaker than set theory.
As to the first question; I believe what is going on is the following (hopefully someone will point it out if I'm wrong); We work within a meta theory, such as PRA (Primitive Recursive Arithmetic). The exact meta theory used is of interest to certain people, but is not really necessary for the purposes of this question. 
Now we have way of talking about what it means for $ZFC$ to prove something. We develop model theory inside of ZFC the usual way. Now Jech is saying: $ZFC\vdash({\varphi}^{(M,E)}\leftrightarrow{(M,E)\models{\ulcorner\varphi\urcorner}})$. Here inside of $ZFC$ we have developed the formal theory of (a copy of) ZFC. So we assume that $\ulcorner\varphi\urcorner$ is associated in some canonical way to $\varphi$ (The formula $\varphi$ is actually represented by a code (a unique natural number) in the meta theory. Now $ZFC$ also has access to a version of the natural numbers, then we are implicitly assuming that the code in the meta theory is the "same as the" code in the formal copy of $ZFC$ in $ZFC$).
