Consistency proof in $\mathrm{ZFA}$ Suppose we work inside a model $M$ of $\mathrm{ZF}$ and we prove that there exists a model of $\mathrm{ZFA}$ that satisfies $\mathrm{Con}(T)$, where $T$ is any theory stronger than $\mathrm{PA}$. Would that mean that $M \models \mathrm{Con(T)}$?
 A: Yes. Though I do not see how you'd get a model of $\mathsf{ZFA}$ in an arbitrary model of $\mathsf{ZF}$, unless you mean that you can, from the original model $M$, obtain a new model, probably class-sized from the point of view of $M$. 
Anyway, if the $\mathsf{ZFA}$ model $N$ satisfies $\mathrm{Con}(T)$, then it sees a model $P$ of $T$. We thus have $M\models N\models P\models T$ (or just $N\models P\models T$, depending on how one goes about getting $N$ from $M$). The point is that if $N\models P\models T$, then there is a $P^*$ that is really a model of $T$--possibly class sized from $M$'s perspective. (And in the situation of $M\models N\models P\models T$, simply iterate this procedure.)
To see this, recall that a model is a set and some constants, relations, and functions. We define the universe of $P^*$ as the set of $t\in N$ such that $N\models$"$t\in P$". Similarly, we define $<^{P^*}$ as the collection of all pairs $(a,b)$ such that $N\models$"$a,b\in P$ and $P\models a< b$". Similarly for the constants $0,1$ for the sum and multiplication functions.
One then checks (easily) that for each axiom $\phi$ of $T$, we have $(P^*,<^{P^*},0^{P^*},1^{P^*},+^{P^*},\times^{P^*})\models\phi$ because $N\models P\models \phi$. Note that, for exmaple, $N\models P\models \mathsf{PA}$ in an assertion about what $N$ thinks $\mathsf{PA}$ is, not about $\mathsf{PA}$ itself. Luckily for us, any standard integer and so any standard formula is unambiguously interpreted in these models, so for any true axiom of $T$ we can assert the claim above, even if $N$ has non-standard integers and so thinks that $P$ satisfies "axioms" that are not even true formulas. 
If the discussion takes place within $M$, the resulting model $P^*$ is in $M$, and so $M\models\mathrm{Con}(T)$. If $N$ is merely definable, one has to check that the $P^*$ one obtains (definable from $N$'s viewpoint) is actually a set from $M$'s perspective, but this is easy here: If $N\models$"$a$ is a set" (as it would be the case if $a=P$ is a model of $T$ from $N$'s point of view), then $a^*$ (defined as above) is truly a set (from $M$'s perspective).--Unless is defined in a rather bizarre manner from $M$, so that it is not set-like, which is not what one usually means here.
(For a nice example of this interplay between models and "codes for models", see this blog post of mine on a proof by Woodin of Gödel's second incompleteness theorem.)
