How to prove from ZFC that the intersection of any non-empty set exists?

It is an axiom of ZFC that $\cup x$ exists for any set $x$, where $\cup$ denotes union. But how does one prove that for any non-empty set $x$, the intersection $\cap x$ exists? We need $x$ to be non-empty, because $\cap \emptyset$ would be the set of everything, which does not exist in ZFC.

Solution 1:

It is a subset of $\cup x$. Recall that $$\cup x=\{ z\mid \exists y(z\in y\wedge y\in x)\}.$$ The intersection is $$\cap x=\{z\in \cup x\mid \forall y( y\in x\rightarrow z\in y)\}.$$ This is a set by the Axioms of Union and Separation.

In fact, this definition allows you define the intersection of an empty family; the issue is that it is equal to $\varnothing$ (since $\cup\varnothing = \varnothing$), so then you run into issues with associativity.