 Embedding of first-order structures

An embedding of first-order structures is an injective function preserving function symbols and constants and both preserving and reflecting every relation symbol. Its image is a substructure. Satisfaction of an atomic diagram of a structure in an expansion gives such an embedding of first-order structures by sending each named element to its new interpretation; literal inclusion requires fixing the interpretations of those names.