lo.logic - Is there formal definition of universal quantification?

From wikipedia quantification has meaning:

In logic, quantification is the
binding of a variable ranging over a
domain of discourse

Is there any formal "definition" of universal quantifier for example using definition of domain of discourse?

I mean a formula build without universal quantifier, and existential one which has the same meaning if referenced to defined domain of discourse?

For example:
Suppose we use domain of discourse (DoD) given by sentence $ U = { x|phi(x) }$ for some $phi(x)$. Then naively we may wrote:

($forall (x in U) Phi(x) ) equiv ( { x|phi(x) } => Phi(x) )$

In words: to say that some property follows for every x in DoD is the same as to say that if x is chosen from DoD then has this property.

We may try also the folowing one:
($forall (x in U) Phi(x) ) equiv (( { x|phi(x) } => Phi(x) ) => (phi(x) <=> Phi(x) ))$

In words: to say that some property follows for every x in DoD is the same as to say that $phi$ and $Phi$ are evenly spanned.

Do You know any reference for such matter?

---

Gabriel: Yes, I agree that from formal point of view in mathematical practice DoD is a set and to extend it to bigger universe usual is done by pure formal way and may be changed to some additional axioms etc. But this is some kind of mathematical practice: "near every decent theory as far as we know is defined for DoD to be set or smaller but as it works also for proper classes we are trying to write it in a way". But then we omit important statement: every time DoD has to be defined and additional axioms about it existence, definition,properties has to be added to the theory. I am only a hobbyist but I do not know any theorem which states: structure to be DoD for formal theory over countable language has to have "this and this" property. Of course for example as in formula ${ x|phi(x)}$ we may require that $phi(x)$ has some property. For example we may require that it is in first order language. Or in second order. Or in finite order language etc. For me is rather clear that it cannot be whatever I like. As far as I know we do not have any theory for that. But maybe I am wrong?

So my question is: what is that mean "for all" in a context of different definition of DoD ( as well as "there exists"). Do we have clear meaning what it means for very big universes? We use some operator here named "for all" but have we possibility to define its meaning in syntactical way? If not, may we be sure that meaning of sentence "for all" is clearly defined?

I suggest this is example of Incomplete Inductive reasoning about possible ways of using general quantifier in mathematics. Moreover I suppose, even after reading something about Hilbert epsilon calculus that quantifiers has usual only intuitive meaning, that is its definition is far from such level of formality as for binary operation $in$ for ZFC for example, where it may be anything (for example in von Neumann hierarchy of sets "model" of ZFC it is order). When we try to define formal theory we want to abstract from the "meaning" of the symbols and give only pure syntactical rules for them. As far as I know ( but I know not much) I do not know such definition for quantifiers, even in epsilon Hilbert calculus for example, because it omits the area of possible, acceptable or correct definitions of domain of discourse.