I'm reading Nik Weaver's Forcing for Mathematicians. This is one of the exercises.
Let $P$ be a forcing notion, let $G$ be a generic ideal of $P$, and suppose $G \in \mathbf{M}$. (As we noted at the beginning of the chapter, this can only happen if $P$ is trivial.) Prove that $\mathbf{M}[G] = \mathbf{M}$.
Note that $\mathbf{M}$ is a countable transitive model of ZFC. Also, that $\mathbf{M} \subseteq \mathbf{M}[G]$ in general is proven in the book, so only the other direction remains.
I went on to prove that $g_1 := \bigcup G$ was an element of $G$, so there existed an element that was the extension of every other element. This gives
$$\tau^G = \{\sigma^G; \sigma \in \tau^{-1}(G)\} = \{\sigma^G; \sigma \in \tau^{-1}(g_1)\}$$
for all $P$-names $\tau$. I'm not exactly sure how I should finish. I think a simple induction on name rank should work: first note that $\tau \in \mathbf{M}$ by definition, then take the definable subset of all ordered pairs such that the second element is $g_1$ and then take the function mapping this subset to the set of all first elements of these pairs. With that I basically get that $\{\sigma; \sigma \in \tau^{-1}(G)\} \in \mathbf{M}$. After that, I just map $\sigma$ to $\sigma^G$ (this is a function of $\mathbf{M}$ by inductive hypothesis, right?) and I have that $\tau^G \in \mathbf{M}$.
But then I realized that all of this could have been done without defining $g_1$ and just working with $G$ directly. It should still work okay, as $G$ is an element of $\mathbf{M}$. Then I'm done. But I didn't use the fact that $P$ is trivial at all here, so I'm confused.
Also, I invoke quite a few of the axioms of ZFC. I assume a similar result has to hold in some weaker systems. For example, doesn't a similar result hold in ZFC without the replacement axiom? My proof uses it a lot, so I'm not sure. Please let me know if I made a big mistake somewhere here.
I'm not familiar with Weaver's notation so I checked the book, but still don't understand why $g_1$ must be an element of $G$. Anyway, as you say we don't really need $g_1$. The logic is this, when doing forcing we fix a countable transitive ground model $\mathbf{M}$, choose some generic ideal $G$, and form the extension $\mathbf{M}[G]$ using the name evaluation map $\sigma\mapsto\sigma^G$; this is carried out in $V$, the ambient universe, or the "real world". But if $G\in\mathbf{M}$, then we can also evaluate names in $\mathbf{M}$, and by absoluteness the result is the same as in $V$, so $\mathbf{M}[G]\subseteq\mathbf{M}$.
The whole machinary of forcing (not just this particular result) does go over systems much weaker than ZFC. However, the map $\sigma\mapsto\sigma^G$ is defined by transfinite recursion, for which you want at least some amount of replacement. Kripke-Platek set theory is more than enough; I believe it even works over many subsystems of second-order arithmetic.