 Finite relation closure for set-theoretic coding

A useful finite conjunction of closure assertions requires empty set, pairing, set union, set difference, Cartesian products, all finite tuple domains $A^n$, and the following operations on their relations: relative complements, intersections, coordinate projections and pullbacks along finite coordinate maps, together with equality and membership restricted to $A^2$. The arities and maps are quantified objects, so these requirements form finitely many first-order formulas, not an infinite schema. In a transitive set, individual finite tuples exist by pairing and union, making the tuple-domain assertions correct externally. Atomic truth relations, Boolean operations and projection then compute the truth table of each coded first-order formula correctly by finite induction. Thus satisfaction for a set structure and the relation $B=\mathrm{Def}(A)$ are absolute for shared arguments. Every nonzero limit level of the relative constructible hierarchy is closed under these operations, since each result can be defined at finitely many subsequent stages.