Formalizing "isomorphism preserves everything" using language of logic In many areas of mathematics there is a notion of isomorphism, which is a map that preserves some structure – an algebraic structure, a topology, a sheaf etc. It is "obvious" that every isomorphism of given structures preserves everything defined by the structures. For example:
–homeomorphism preserves borelianity (image of Borel set is a Borel set);
–isomorphism of algebraic varieties preserves rational maps (composing rational map with isomorphism gives a rational map);
–isometry of metric spaces preserves balls (image of a ball is a ball of the same radius) – and it is not true for every homeomorphism, as the definition of "ball" uses the metric structure, not only the topological one.
All the above and many similar statements can be easily proved by hand, by writing all the definitions and proving, step by step, that isomorphism preserves every used object. Thus we can actually skip all those proofs and say it is all obvious.
The questions is: is there any theorem of mathematical logic that formalizes all such arguments? I would expect it to be of form "for any two sets X, Y with some structures, if some function $f:X\to Y$ preserves the structures, then every statement true for the first one and defined using the structure is true for the other after applying appropriate changes (like $A \mapsto f(A)$ for any $A\subset X$)".
 A: Generally it can be said that if a property of either a structure or particular elements in it can be expressed at all by a logical formula over the language in question, then it is preserved by isomorphisms.
Here "the language in question" means the formula can only speak about things that the isomorphism is required to preserve, but the formula can be either first or higher order.
This is nice and tidy in many common cases, though minor subtleties arise for cases like metric spaces where the formulas need to speak about real numbers in addition to points in the space.
Formally this can to a large extent be handled by extending the language with a new sort for real numbers, and constants for every real -- but it may be slicker to extend the notion of "logical language" with some kind of pseudo-function letters that always produce real results (or whatever one needs) and then allow one to have atomic formulas of the form $(f_1[t_{11},\ldots,t_{1n}],\ldots,f_k[t_{k1},\ldots,t_{kn}]) \in A$ where $A$ is any fixed subset of $\mathbb R^k$ at the metalevel.
I'm not aware of this having been written down in so many words anywhere -- but something like it is what I imagine when it is said "it is obvious that such-and-such property is preserved by isomorphisms, because it can be defined with reference only to the primitive notions that isomorphisms are required to preserve".
