There is a precise way to formalise this.
We want to speak of sets not as collections of particular mathematical objects but as a bag of featureless dots. These bags of dots are related to each other by functions, which also relate dots in one bag to dots in another.
In order to do this, we propose a language for discussing sets. Capital letters will represent sets, and lowercase variables will represent functions between sets.
We define a "nice proposition about sets" as any proposition that can be generated from the following rules:
- For any sets $A, B$ and any function variables $f, g: A \to B$, $f = g$ is a nice proposition
- We can combine nice propositions $\phi, \psi$ using the operators $\land$, $\lor$, $\neg$, and $\implies$ to get another nice proposition
- $\top$ and $\bot$ (that is, true and false) are nice propositions
- If $\phi(A)$ is a nice proposition, where $A$ is a set variable, then $\forall A (\phi(A))$ is a nice proposition (and similarly for $\exists$)
- For all set variables $A, B$, if $\phi(f)$ is a nice proposition (where $f : A \to B$ is a function variable), then $\forall f : A \to B (\phi(f))$ is a nice proposition (and similarly for $\exists$)
Finally, in our language, we can form new functions from old ones using function composition and also discuss identity functions. Note that we will only discuss function composition when we know that the functions are composable syntactically.*
Note that we very deliberately avoided two things. First, there is no mention of the elementhood relation at all. Second, there is no way to compare two sets for equality, nor is there a way to compare two functions for equality unless the two have the same domain and codomain. This is deliberate. Also note that all variables here have specific types, and that we rely on these types to determine whether we can discuss equality.
Despite this avoidance, it is both an empirical fact and a (rather complicated) theorem that all propositions with no free variables can be translated to a "nice proposition about sets". For most mathematically useful propositions, the translation is relatively intuitive for those comfortable with category theory.
To get around the restriction that we not discuss elements directly, we can fix some 1-element set $1$ and discuss elements of $A$ as functions $1 \to A$. We denote the situation $x : 1 \to A$ as $x :\in A$. When we have $x :\in A$ and $f : A \to B$, we write $f \circ x$ as $f(x)$ (note that $f(x) :\in B$). Note that this is enough to define, for example, a group (as a set $G$, together with a function $- \cdot - : G^2 \to G$ which satisfies the group laws**).
We thus have the following theorem:
Big Theorem. Consider some nice proposition $\phi(G)$ - that is, some statement $\phi$ where the group variable $G$ occurs free. Then we can prove the following statement: "For all groups $G_1$, $G_2$, if $G_1$ and $G_2$ are isomorphic and $\phi(G_1)$, then $\phi(G_2)$."
Let us discuss how this relates to your example of $\mathbb{Z}$ and $2 \mathbb{Z}$.
We may try to define $\phi(G)$ as the statement "$\mathbb{Z} / G$ is the zero group". Then taking $G_1 = \mathbb{Z}$ and $G_2 = 2 \mathbb{Z}$, we see that $\phi(G_1)$ holds but $\phi(G_2)$ is false. This would appear to violate our Big Theorem.
To understand what's going on, we need to understand exactly what is going on with the statement $\phi(G)$. Note that in this statement, it is necessary for $G$ to be a subgroup of $\mathbb{Z}$ - in particular, it must be a subset. That is, we must have $\forall x \in G (x \in \mathbb{Z})$.
Of course, we cannot express such a statement as a nice proposition about sets, since it relies on the proposition $x \in \mathbb{Z}$, which is not a nice proposition. So we have to approach things a bit differently.
Rather than forcing $G$ to be a subgroup in the traditional, literal sense, we instead make $G$ a subgroup of $\mathbb{Z}$ in a more general sense. That is, we discuss a group $G$, together with some injective group homomorphism $i : G \to \mathbb{Z}$. In other words, we discuss $G$ together with a specific way that $G$ is a subgroup of $\mathbb{Z}$.
This makes it clear that $\phi(G)$ is not really just a proposition about $G$ - it's also about the way that $G$ is a subgroup of $\mathbb{Z}$. So it's really a proposition $\phi(G, i : G \to \mathbb{Z})$. Because $\phi$ depends on a secondary variable $i$, we see that we cannot apply our Big Theorem to conclude that $\phi(\mathbb{Z}) \iff \phi(2 \mathbb{Z})$.
If it were the case that the isomorphism $w : \mathbb{Z} \to 2 \mathbb{Z}$
"played nicely" with the inclusion maps $i_1 : \mathbb{Z} \to \mathbb{Z}$, $i_2 : 2 \mathbb{Z} \to \mathbb{Z}$ (that is, if $i_1 = i_2 \circ w$), then we would be able to conclude that $\phi(\mathbb{Z}, i_1) \iff \phi(2 \mathbb{Z}, i_2)$ using a generalisation of our Big Theorem. But of course the isomorphism does not play nicely with the inclusion maps.
*An astute observer will note that this is exactly the language of category theory. A "nice proposition about sets" is just some statement about the category of sets (which avoids discussing equality of objects).
**Technically, we need a way to define $G^2$ first. This is done using the categorical definition of the universal property of the product.