Correspondence theorem for rings. Could someone provide a reference that includes a full and honest proof of the Correspondence Theorem for rings?

Let $A$ be a multiplicative ring with identity and $I$ an ideal of $A$. There is a one-to-one correspondence between the ideals of $A$ that contain $I$ and the ideals of the quotient ring $A/I$.

 A: Consider rings $R, R'$ (commutative, with unity) and a ring homomorphism $R \overset{\varphi}{\to} R'$.
For any ideal $J$ of subring $\varphi(R)$, clearly $\color{green}{\varphi(\varphi ^{-1} (J)) = J}$.
Also, for any ideal $I$ of $R$,  $\varphi ^{-1} (\varphi(I))$ $= \lbrace t \in R : \varphi(t) = \varphi(i) \text{ for some } i \in I \rbrace$ $ = \lbrace t \in R : t - i \in \ker(\varphi) \text{ for some } i \in I \rbrace$ $ = I + \ker(\varphi) $.
That is, for any ideal $I$ of $R$, $\color{green}{\varphi ^{-1} (\varphi (I)) = I + \ker(\varphi)}$.
But ideal $I + \ker(\varphi) = I$ if and only if $I \supseteq \ker(\varphi)$. This suggests :
Th: Let $R \overset{\varphi}{\to} R'$ be a ring homomorphism. There is a bijection
$$\lbrace \text{ideals of } R \text{ containing } \ker(\varphi)\rbrace \leftrightarrow \lbrace \text{ideals of } \varphi(R) \rbrace, $$
where $I$ in LHS is mapped to $\varphi(I)$.
Pf: Call LHS $\mathbf{A}$ and RHS $\mathbf{B}$. Define $\mathbf{A} \overset{f}{\to} \mathbf{B}$ by $I \mapsto \varphi(I)$, and $\mathbf{B} \overset{g}{\to} \mathbf{A}$ by $J \mapsto \varphi ^{-1}(J)$.

These are well-defined : $I \in \mathbf{A}$ implies $\varphi(I) \in \mathbf{B}$, and $J \in \mathbf{B}$ implies $\varphi ^{-1}(J) \in \mathbf{A}.$

For any $J \in \mathbf{B}$, $(f \circ g)(J)$ $= \varphi(\varphi ^{-1}(J))$ $=J$, so $f \circ g = \text{id} _{\mathbf{B}}$.
Similarly for any $I \in \mathbf{A}$, $(g \circ f)(I)$ $= \varphi ^{-1} (\varphi(I))$ $= I + \ker(\varphi)$ $=I$, so $g \circ f = \text{id} _{\mathbf{A}}$ too.
A: My reference is this post.  Note that it is not necessary for $A$ to have an identity.

Let $\mathscr{C}$ and $\mathscr{D}$ denote, respectively, the collection of ideals of $A$ containing $I$, and the collection of ideals of $A/I$.
Define: $f:\mathscr{C}\to\mathscr{D}$ by $f(J) = \{a + I \mid a\in J\}\subset A/I$.
Define $g:\mathscr{D}\to\mathscr{C}$ by $g(\mathcal{J}) = \{a\mid a+I \in \mathcal{J}\} \subset A$.
(I omit the proofs that these give ideals, but these follow trivially from the definitions.)
If $\mathcal{J}\in\mathscr{C}$, then $(f\circ g)(\mathcal{J}) = \{a+I \mid a\in g(\mathcal{J})\} = \{a+I \mid a+I\in\mathcal{J}\} = \mathcal{J}$
.
If $J\in\mathscr{C}$, then $(g\circ f)(J) = \{a\mid a+I \in f(J)\} = \{a \mid a+I=b+I\text{ for some } b\in J\}$ $= \{a \mid a\in b+I\text{ for some } b\in J\}$.
This last set clearly contains $J$.  But $a\in b+I \implies (a-b)\in I\subset J \implies a=b+J\implies a\in J$.  So $(g\circ f)(J) = J$, and we have shown that $f$ and $g$ establish a bijection.

It probably doesn't get proved like this very often, because it's a lot shorter if we're allowed to use a few definitions.  It is, however, the same proof.
If $f:A\to B$ is a surjective ring homomorphism, and $J$ is an ideal of $A$ containing $\ker f$, then $f(J)$ is an ideal of $B$, because $Bf(J) \subset f(AJ) \subset f(J)$.
If $J'$ is an ideal of $S$, then $f^{-1} (J')$ is an ideal of $R$.
We have $f(f^{-1}(J')) = J'$ trivially, and $f^{-1} (f(J)) = J + \ker{f} = J$.
