Htykuut

As far as I know, in a nutshell, if for a formal system $mathcal{F}$ we have $vdash_mathcal{F} exists! y phi(y,x_1,cdots,x_n)$ then we can safely introduce a new formal system $mathcal{F}'$ that differs from $mathcal{F}$ because it has a new function symbol $f$ and a new axiom $vdash_mathcal{F'} y=f(x_1,cdots,x_n) iff phi(y,x_1,cdots,x_n)$. More precisely, the new system $mathcal{F'}$ is a conservative extension of $mathcal{F}$.

However, sometimes it happens that new symbols are introduced even if the existential premise "$exists! y ldots$" is only "partial". For example, by studying $mathcal{ZFC}$, I noted that usually intersection is only "partially defined", namely I have only $xneq emptysetvdash_mathcal{ZFC} exists! y forall u(uin yiff forall vin x(uin v))$. By "partial", I mean that the case $x=emptyset$ is escluded. In this case, the above scheme is not fulfilled, and I cannot introduce the new function symbol $bigcap$ since this is not defined for $emptyset$. Therefore, here is my first question. 1) Is there a more general scheme? Namely, is there a more general way to conservatively extend a system involving partial definitions? (I think the answer is no, but I need a confirmation)

An other common way to define intersection is to use separation, union and extentionality axioms to prove $vdash_mathcal{ZFC} exists! y forall u(uin yiff uin bigcup x land forall vin x(uin v))$. This solution produces a complete definition, and therefore I can extend $mathcal{ZFC}$ introducing the new function symbol $bigcap$ by exploiting the scheme reported above. However, this solution has different drawbacks, due to the fact that it imposes $bigcap emptyset=emptyset$. For example, it is not true that $vdash_mathcal{ZFC} asubseteq b implies bigcap b subseteq bigcap a$. But, this seems an apparent limitation, because I can state all the theorems (properties) about a certain $bigcap x$ by simply adding the hypothesis $xneqemptyset$. For example, I can state $aneqemptyset,bneqemptysetvdash_mathcal{ZFC} asubseteq b implies bigcap b subseteq bigcap a$.
Actually, for this case, I could omit the hypothesys $aneqemptyset$, but the sense is to eliminate any occurrence of $bigcapemptyset$ from any reasoning, since I accept this patological definition only because I need to define the symbol $bigcap$ for any member of the universe, not because I actually want to use it for patological cases. Therefore, here is my second question. 2) Is this way to procede correct (in general, not only for the intersection symbol)?

Thank you!