Cfrgtkky

One of the axioms of ZF set theory is the axiom of union:
$$(forall x)(exists y)(forall z)(zin y iff (exists t)(zin t & tin x)).$$
The axiom of union (together with the axiom of extensionality) guarantees that the operation $$xmapstobigcup x$$ can be defined for all sets and indeed captures our intuition of the union of all elements of $x$.

On the other hand intersection, understood as a common part of all members of a set, cannot be defined since $bigcapemptyset$ poses a problem. However, what is stopping us from using the axiom scheme of separation and defining
$$bigcap x :={yinbigcup x | (forall z)(zin xRightarrow yin z)},$$
which is a correct instance of the axiom scheme of separation and captures the notion of the intersection of all elements for nonempty sets $x$, while for an empty set we have clearly $bigcapemptyset = emptyset$ (since $bigcupemptyset = emptyset$)?

Addressing comments and to be more precise: how to define an intersection of all members of a set in ZF (please provide a formula in a language of ZF) such that the induced operation of intersection is undefined for the empty set?

I ask because I saw that people have this definition in mind (instead of "mine" presented above), but rarely write it down and just go on just claiming that
$$bigcap x$$
is possible to define for nonempty sets $x$, and undefined for $emptyset$ (i.e. see chapter 5 in "Notes on logic and set theory" by P. T. Johnstone).

Let's pretend that you are a new student to set theory. Let's assume that you understood the primitive notions of membership and equality, what formulas are (in the language of Set Theory), and the following nonlogical axioms: extensionality, existence of empty set, separation, pairing, union.

Now let's develop the notion of intersection.

Remark. For each nonempty collection $mathcal{C}$ of sets, there exists a unique set, denoted $$bigcapmathcal{C}qquadtext{or}qquad{x:(forall Ain mathcal{C})[xin A]},$$
whose elements are exactly those elements $x$ such that $xin A$ for every $Ainmathcal{C}$.

Indeed, consider ${xin A_0:(forall Ain mathcal{C})[xin A]}$ where $A_0$ is any fixed element of $mathcal{C}$.

Definition.
Let $mathcal{C}$ be a nonempty collection of sets.
The intersection of $mathcal{C}$ is $bigcapmathcal{C}$.

Definition. Let $X$ and $Y$ be sets. The intersection of $X$ and $Y$, denoted $Xcap Y$, is $bigcap{X,Y}$.

End of development.

Notice that $bigcapmathcal{C}$ is only defined once it is established that it is nonempty.

Side Note: It is unreasonable to define an infimum operator for an arbitrary set $X$. The set $X$ does not even have an ordering! It is pointless to try. Only once $X$ has an established partial ordering should one continue to define the infimum operator. But even then the infimum may not exist in all cases. That is why the typical work-around is to instead focus one's attention to a complete lattice, or even better, consider the completion of $(X,preceq)$ (if it is unique up to isomorphism), or resign oneself that some collections have no infimum.

I use infimum here because that is essentially what $bigcap$ is---an infimum of a collection of sets under the established ordering $subseteq$. However, as we are quite aware, there is no infimum for $varnothing$.

I'm not exactly sure if I'm understanding the question correctly but I will try and give an explanation based on my understanding.

We certainly can define $bigcap$ as you have nicely shown. I don't think you even need the axiom of union since the intersection is in every set in $x$. Now the reason it can be defined this way means we don't need to have it as an axiom (just pointing that out in case there was confusion).

The reason we don't (usually) define the intersection in the way we do for union (i.e. as an intersection of a single set, understood as a family of sets, as it is done for union) is IMO that it's rarely used and also precisely because it's not an axiom.

Writing $bigcap_{xin X}x$ is easy enough and we could do it for union aswell. But the notation used for the axiom is a little neater.

But we fairly rarely take intersection of whole families, or at least I can't really think of many situations we do so.

Another reason why we do have the $bigcup x$ notation for union is that there is parts of set theory where it does help. That is when we create transitive closures of different kinds. Essentially sometimes we are trying to make sure we have a nice big enough set where everything we need to do can be done. That is that the set we work in contains everything we could possibly need to talk about has nice properties and is still a Set as opposed to a proper class.

I reject this as counterintuitive.

The smaller the set $a$ the larger the set $cap a$ because the number of demands on $x$ to be element of $cap a$ decreases if $a$ gets smaller.

But then suddenly if $a$ is the smallest set (empty) and all demands are vanished then no $x$ can pass anymore?... Weird situation!

What also goes lost (and is in my eyes very valuable) is the convention that: $$capvarnothing:=X$$ when we are working in some universal set $X$.

Next to that I do not see (yet) any advantages.

PS. I use $cap$ instead of $bigcap$ here, seeing $cap$ as an operator on non-empty sets and seeing $bigcap_{xin a}x$ as another notation of $cap a$.

That is also a matter of taste of course.