A question on metamathematics of forcing. This question might be a duplicate but i have found no other questions related to this so here we go. 

In kunens (An introduction to independence proofs) and Nik weavers (forcing for mathematicians) books there is a way to deal with c.t.m.s as follows:  Construct another theory named $\text{ZFC}^+$ which it's language is that of $\text{ZFC}$ but has an additional constant symbol $M$. And it's axioms are:1) All axioms of $\text{ZFC}$.  2) The single assertion that $M$ is countable and transitive.  3) All axioms of $\text{ZFC}$ relativized to $M$.
Then we prove that $\vdash \text{Con}(\text{ZFC}) \rightarrow \text{Con}(\text{ZFC}^+)$

Now my question: Since we know that $\text{ZFC}^+$ contains a model of $\text{ZFC}$, we can say that $\text{ZFC}^+ \vdash \text{Con}(\text{ZFC})$ and we have $\vdash \text{Con}(\text{ZFC}) \rightarrow \text{Con}(\text{ZFC}^+)$ so we get $\text{ZFC}^+ \vdash \text{Con}(\text{ZFC}^+)$, a contradiction with incompleteness?
 A: No, $\text{ZFC}^+$ does not prove $\text{Con}(\text{ZFC})$.  It does not prove that $M$ is a model of ZFC.  For each individual axiom $\varphi$ of ZFC, it proves that $M\vDash\varphi$.  But it does not prove the single sentence $\forall\varphi\in\mathrm{ZFC} (M\vDash\varphi)$ which is what it would mean to prove that $M$ is a model of ZFC.
(Note that by the completeness theorem, this means it is possible to have a model of $\text{ZFC}^+$ in which the sentence $\forall\varphi\in\mathrm{ZFC} (M\vDash\varphi)$ is false.  How can this be?  The reason is that in this sentence, $\mathrm{ZFC}$ refers to the set in your model which encodes the set of axioms of ZFC.  If the natural numbers of your model are nonstandard, this set will have elements that do not actually correspond to true axioms of ZFC (since their length is actually a nonstandard natural number).  So, even though $M$ satisfies every actual axiom of ZFC, your model may not think that $M$ satisfies every element of the set it calls ZFC.)
