There is really nothing magical about $\sf ZFC$ that requires dark magic to conjure definitions.
The whole point of foundations using set theory is to give a basic way to translate "usual definitions" into set theoretical objects using some basic "meta-algorithm" for translation. It is true that this algorithm is somewhat limited, but still, if you have a property that you want to abstract then this property is something that can be expressed in something which itself can be (usually) expressed within the set theoretical universe.
So abstraction is not the issue here.
If something is given, for example, the set $\Bbb Z$ and the set $+$ which happens to be a binary operator on $\Bbb Z$ satisfying the properties:
- There is some $x\in\Bbb Z$ such that for all $y$, $x+y=y$.
- For every $x$ there is some $y$ such that for all $z$, $(x+y)+z=z$.
- For every $x,y,z\in\Bbb Z$, $(x+y)+z=x+(y+z)$.
- For every $x,y$ we have that $x+y=y+x$.
Now we want to say that an object with this property is called an abelian group. What is "this property"? It means that there is a set which is non-empty, $G$ and a binary operator on $G$ which will shall denote by $+_G$, and it satisfies these properties, all of which really talk about the existence of certain ordered pairs and triplets inside that binary operator. All this happens within naive set theory, let alone with $\sf ZFC$.