Congruence relation on a first-order structure ($a_i\sim b_i⟹f(\vec{a})\sim f(\vec{b})$)

A congruence relation on a first-order structure is an equivalence relation compatible with each interpreted function and relation. Equivalent input tuples give equivalent function outputs, and an atomic relation has the same truth value on equivalent input tuples. This compatibility makes the functions and relations well-defined on the quotient set. In a Henkin term model with equality, membership of a formal equality in the maximal consistent theory gives precisely the equivalence relation used for this quotient.