One of the most basic insights about mathematical structures is that we can rename their elements without fundamentally changing the structure.
Question. How do we actually formalize this observation in its maximum generality?
Here's an attempt I made, taking topological spaces as an example.
Claim: Suppose $X$ and $X'$ are sets and $f : X \rightarrow X'$ is a bijection. Then for all topological spaces $(X,\tau),$ there exists a unique topological space $(X',\tau')$ such that $f$ is a homeomorphism $(X,\tau) \rightarrow (X',\tau').$
Proof sketch.
Existence: Just take $\tau' = \{\;f(B) \mid B \in \tau\;\}.$
Uniqueness: Suppose we have distinct $\tau',\tau''$ satisfying the condition. Then: $$B \in \tau' \Leftrightarrow f^{-1}(B) \in \tau \Leftrightarrow f(f^{-1}(B)) \in \tau''$$
So $\tau'=\tau'',$ a contradiction.
Remark. I wasn't sure how to tag the question. Please feel free to edit.
It is called transport of structure. Formally, take two sets $X,Y$ with a bijection $f \colon X \to Y$. Suppose that $X$ is the base set of a $\mathcal L$-structure $\mathfrak X$. Then there exist a $\mathcal L$-structure $\mathfrak Y$ with $Y$ as base set defined by : for every constant symbol $c$, function symbol $\phi$ and relation symbol $R$ of the language $\mathcal L$, $$c^{\mathfrak Y} := f(c^{\mathfrak X}),$$ $$\phi^{\mathfrak Y} := (y_1,\dots,y_k) \mapsto f(\phi^{\mathfrak X}(f^{-1}(y_1),\dots,f^{-1}(y_k))),$$ $$R^{\mathfrak Y} := \{ (y_1,\dots,y_k) \in Y^k : (f^{-1}(y_1),\dots,f^{-1}(y_k)) \in R^{\mathfrak X}\}.$$
Moreover, this structure makes $f$ an isomorphism of $\mathcal L$-structures. By definition of "isomorphism of $\mathcal L$-structures", it is unique.