Łoś–Tarski preservation theorem

Statement

Let T be a theory in a first-order language L and Φ ( x ¯ ) a set of formulas of L . (The set of sequence of variables x ¯ need not be finite.) Then the following are equivalent:

1. If A and B are models of T , A ⊆ B , a ¯ is a sequence of elements of A . If B ⊨ ⋀ Φ ( a ¯ ) , then A ⊨ ⋀ Φ ( a ¯ ) .
   ( Φ is preserved in substructures for models of T )
2. Φ is equivalent modulo T to a set Ψ ( x ¯ ) of ∀ 1 formulas of L .

A formula is ∀ 1 if and only if it is of the form ∀ x ¯ [ ψ ( x ¯ ) ] where ψ ( x ¯ ) is quantifier-free.

Note that this property fails for finite models.