How do I get the existence of a set in ZFC following Jech? I am learning some set theory and logic on the side and am looking Jech's book, "Set Theory". At the moment, I am learning the basic axioms, and what I can and cannot do with them. Most of the axioms are of the form, if such and such set exists, then so does this set (the power set axiom, If X exists, so does it's power set). These sets by themselves do not  give us actual sets to deal with, so the entire theory could be empty. Thus we have the axiom of infinity which states, $\exists S (\emptyset\in S \wedge (\forall x\in S)x\cup\{x\}\in S)$.
However, this axiom seems to already give the existence of the empty set before one can get the infinite set, $S$. So do we need the empty set in existence before we can state this axiom or does it come from some other place. Again it does not seem to come from the other axioms.
 A: You can replace $\emptyset$ with $\{ x\in S: x\neq x\}$ in the axiom of infinity, because of the separation axiom. This way, the axiom of infinity implies the existence of all sets all by itself.
A: The usual formalizations of first-order logic implicitly assume a non-empty domain of discourse. Knowing that, one can argue informally as follows: let $D$ be any set, and let $E=\{x\in D:x\ne x\}$. The existence of $E$ follows from comprehension, and it’s not hard to prove that $\forall x(x\notin E)$.
A: The symbol $\emptyset$ is not part of the formal language of ZFC, so from the strictest viewpoint the subformula "$\emptyset \in S$" is not even syntactically valid in ZFC. 
One way to handle that problem is to prove there is a set that has no members, as Brian M. Scott indicates, and then make a definitional expansion of ZFC to add a constant symbol $\emptyset$ for this set.
Another way to handle it, without making a definitional expansion, is to just mentally replace "$\emptyset \in S$" with something like "$(\exists z)[(\forall w)[\lnot (w \in z)] \land z \in S]$". Obviously this makes the axiom much harder to read, so writing $\emptyset \in S$ is a convenient abbreviation. 
This same issue comes up in many formal settings: when someone uses a symbol that is not in the formal language, but where you know the intended definition for the symbol, you can simply interpret the formula as an abbreviation for a longer formula that does not use the symbol. For example, the definition in $\{z \in \mathbb{N} : z\text{ is even}\}$ is not a formula of ZFC, but it is an abbreviation for $(\exists w \in \mathbb{N})[z = w + w]$, which in turn is an abbreviation for a much longer formula that does not include the symbols "+" or "$\mathbb{N}$". In most settings the author will not comment much on this sort of thing unless it is unclear that there is a definition in the language of set theory or unless it matters which specific definition is used. 
