Models of the elementary diagram yield elementary embeddings

For an $L$-formula $\varphi$ and tuple $\bar{a}$ covering its free variables, replace those free variables by the corresponding constants, obtaining a sentence $\varphi ({\bar{c}}_{\bar{a}})$. A constant has no free variables, so each replacement is free for its variable; replacements for distinct variables do not alter earlier inserted constants. Iterating F3 and then F4 shows that ${\mathcal{M}}_M\models \varphi ({\bar{c}}_{\bar{a}})$ iff $\mathcal{M}\models \varphi [\bar{a}]$, and for any expansion $\mathcal{N}$ of $\mathcal{B}$ it shows $\mathcal{N}\models \varphi ({\bar{c}}_{\bar{a}})$ iff $\mathcal{B}\models \varphi [(c_a^{\mathcal{N}}{)}_{a\text{ in }\bar{a}}]$. For the empty tuple this is just reduct invariance.

Conversely let $e$ be elementary and interpret each name by $e(a)$. For a sentence $\sigma$ of $L_M$, only finitely many new constants occur. Replace the distinct occurring names by distinct variables absent everywhere from $\sigma$, giving an $L$-formula $\theta$; such variables exist because a finite word uses finitely many variables and the variable supply is $\omega$. No binder in $\sigma$ binds any of the newly introduced variables. Substituting the corresponding constants back into those free positions recovers exactly $\sigma$. By F3, its truth in ${\mathcal{M}}_M$ is truth of $\theta$ at the corresponding tuple from $M$, and its truth in the proposed expansion of $\mathcal{B}$ is truth of $\theta$ at the image tuple. Elementarity equates these truth values. Thus every $\sigma$ in the diagram is true in the proposed expansion, as required. If no new constants occur, use the empty tuple.

For completeness of the inclusion formulation, replace the elements of $B\setminus e[M]$ by the tagged copy $C=\{(M,b):b\in B\setminus e[M]\}$. This is a set by Replacement. If $(M,b)\in M$, then F7 gives the forbidden membership cycle $M\in \{M\}\in (M,b)\in M$, so F9 proves $C\cap M=\mathrm{\varnothing }$. By F8 the map $b\mapsto (M,b)$ is injective. Put $D=M\cup C$ and define $j:B\to D$ by $j(e(a))=a$ and $j(b)=(M,b)$ otherwise. Injectivity of $e$ makes the first clause well defined; the clauses have disjoint ranges and are bijective onto $M$ and $C$. Thus $j$ is a bijection and $j\circ e$ is literal inclusion.

Suppose $\mathcal{N}\models \mathrm{EDiag}(\mathcal{M})$ and define $e(a)=c_a^{\mathcal{N}}$. If $\mathcal{M}\models \varphi [\bar{a}]$, step 1.1 puts the named sentence in the diagram, so $\mathcal{N}$ satisfies it and $\mathcal{B}\models \varphi [e\bar{a}]$. If $\mathcal{M}$ does not satisfy the instance, its named negation belongs to the diagram; thus $\mathcal{B}\models \mathrm{\neg }\varphi [e\bar{a}]$. These two cases prove preservation and reflection. In particular $a\mathrm{\ne }b$ gives $e(a)\mathrm{\ne }e(b)$ by the diagram inequation, and F2 proves that $e$ is an elementary embedding.

Transport the structure along $j$: put $c^{\mathcal{D}}=j(c^{\mathcal{B}})$, $f^{\mathcal{D}}(j\bar{b})=j(f^{\mathcal{B}}(\bar{b}))$, and $R^{\mathcal{D}}(j\bar{b})$ iff $R^{\mathcal{B}}(\bar{b})$. Bijectivity makes these interpretations well defined and total. Term induction shows values are carried by $j$ (variables, constants, then the displayed function identity). Atomic truth is then preserved and reflected, using injectivity for equality and the displayed relation identity. Negation and conjunction preserve this agreement, and an existential witness transfers in either direction by $j$ or $j^{-1}$. Formula induction therefore proves that $j$ preserves and reflects all formulas. Combining with the elementarity of $e$, for every $\bar{a}$ in $M$ truth in $\mathcal{M}$ equals truth in $\mathcal{B}$ at $e\bar{a}$ and hence truth in $\mathcal{D}$ at $j(e\bar{a})=\bar{a}$. F2 gives the required substructure conditions and $\mathcal{M}\prec \mathcal{D}$.