Upon some reflection, what you're doing in a proof like that is not actually defining
x to be a specific object. Instead, what you're doing is defining
x to be a variable that varies over elements of X. (a "general element")
Once you've introduced the variable
x, a definition
A := {x}
is a perfectly good way to define a new variable A. (and makes
A and
x dependent variables)
Then the challenge of the proof is to ensure that your generalized elements are drawn from non-empty sets.
For finitely many such variables, it is enough to show that each individual variable varies over a non-empty domain.
For infinitely such variables, we still need only ensure each individual variable ranges over a non-empty domain. Some variant of the notion of choice function ensures that the entire collection of variables jointly varies over a non-empty domain.
Without the axiom of choice, we are no longer guaranteed that the collection of all our variables varies over a non-empty domain even if each individual one does on its own. It becomes more difficult to make arguments of this form.