Proof by contradiction : about the assumption that there are finitely many primes. To prove by contradiction that there are infinitely many primes, we first assume there are finitely many primes.
It sounds to me that we can consider all primes in $\mathbb{N}$.
Is this assumption possible beacause of a ZFC axiom, that is, we take the set of all primes $\{x\in\mathbb{N}:x\text{ is a prime}\}$ and assume the set is finite?
(I did not know Euclid's proof is a proof by cases, a direct proof method.)
 A: Yes, the axioms of ZFC guarantee the existence of the set of all primes in $\mathbb{N}$.
Indeed, in ZFC the axiom scheme of specification (also known as axiom scheme of separation, or axiom scheme of comprehension) says that:
$$\tag{1}
    \forall w_{1},\ldots ,w_{n}\,\forall A\,\exists B\,\forall x\,(x\in B\Leftrightarrow [x\in A\land \varphi (x,w_{1},\ldots ,w_{n},A)])
$$
where $\varphi$ is any formula in the language of set theory with free variables among $x, w_1, ..., w_n, A$ ($B$ does not occur free in $φ$).
Now, instantiate $(1)$ with $n=0$ and $A = \mathbb{N}$ (it exists in ZFC because of the axiom of infinity), and with the formula $\varphi(x)$ that says that $x$ is prime (it can easily be expressed in the language of set theory).
It yields
$$
\exists B  \, \forall x (x \in B \Leftrightarrow (x \in \mathbb{N} \land x \text{ is prime})) 
$$
So, in ZFC there exists a set $B$ that is nothing but $\{x \in \mathbb{N} : x \text{ is a prime}\}$.

In ZFC, the axiom scheme of specification is not assumed as axiom because it can be derived from another axiom scheme in ZFC, the axiom scheme of replacement, as explained here.
