Prove that intersection of a set is an existing set Prove that $ \bigcap S $ exists for all $S  \neq \emptyset$ using set theory axioms.
I started with $S  \neq \emptyset$ means that there is at least one $B\in S$ but I don't know what to do next and which axioms to use.
Clarification: $ \cap S=\cap_{A\in S} A = \{x| x\in A, \forall A \in S\}$
 A: We know there exists a set $ z\in S\ $  as $ S\neq\phi $. Let $ \varphi(x)\equiv \forall y(y\in S\rightarrow x\in y).\ $  Then choose $y=z$ and  $ \varphi(x)\rightarrow x\in z. $ By the Axiom of comprehension,  we know $ \exists B(\forall x(x\in B\leftrightarrow x\in z\wedge\varphi(x)) $. And $ (x\in B\rightarrow(x\in z\wedge\varphi(x)) $ implies $ (x\in B\rightarrow\varphi(x)) $ and $((x\in z\wedge\varphi(x))\rightarrow x\in B)$ and $(\varphi(x)\rightarrow x\in z)$ implies $(\varphi(x)\rightarrow x\in B) $. Hence $ \exists B(\forall x(x\in B\leftrightarrow  \varphi(x)) $.
A: Let $S\neq \emptyset$ be arbitrary, consider two arbitrary sets $S_0,S_1\in S$ such that $S_0\neq S_1$. Either $S_1$ or $S_0$ is empty, but not both.
If $S_0/S_1$ is empty $S_1\cap S_0=\emptyset$. The empty set exist by ZF. (Technically we are running cases here, but we know what's going on so I will skip the technicality).
If $S_0/S_1$ is not empty, either  $S \cap S_0= S_{\cap}$, meaning the two sets $S_1$ and $S_0$ share an element, and, therefore, $S_{\cap}$ exists.
Or, $S_0/S_1$ is not empty, but $S\cap S_0=\emptyset$ (empty set exists). Therefore, it holds for the base case.
Suppose that $\cap_{0\leq i\leq n}S$ exists.
By the inductive assumption $\cap_{0\leq i\leq n}S=S'$, consider the set $S_{n+1}\in S$ such that $S_{n+1}\neq S_i, i\in[0,n]$;
Either $S_{n+1}$ is empty or not. If it's empty $S'\cap S=\emptyset$ so we are done.
Or, $S_{n+1}$ is not empty:
Then either $S'\cap S_{n+1}=S^*$, hence the intersection exists. Or, $S'\cap S_{n+1}=\emptyset$.
Hence, $\cap_{0\leq i\leq n+1}S$ exists.
Therefore, $\forall S, \cap S$ exists.
