Existential embedding (source code)

= Existential embedding
{title2=$A\preccurlyeq_1 B$}

= 1-embedding
{synonym}

An embedding of <first-order structures> is existential when every existential formula with parameters from the source has the same truth value in the source and target. Forward preservation follows from being a <structure embedding>; reflection is the additional requirement. Applying <compactness theorem> to the target's <diagram of a structure> and the source's <elementary diagram> places the target inside an elementary extension of the source.