Below list the axioms of ZFC assuming FOL.
We start with two primitive notions, which cannot be defined. These being an object called a “set” \{\}, and a relation called “contains” \in.
If two sets have the same members, they are equal:
\forall y \forall z \left[\forall x (x \in y \iff x \in z) \implies y = z\right]
In english, this means for all sets A,B, if for all elements x in A if and only if x in B, then A = B.
We have the following definitions for additional symbols
We denote the following
x \not \in y if \lnot(x \in y)
x \subseteq y if \forall z \in x(z \in y)
x \subset y if (x \subseteq y) \land \lnot(x = y)
Existence Axioms
The following axioms ensure the existence of many fundamental sets.
There is a set with no members:
\exists y \forall x, x \not \in y
For any two sets u and v, there is a set having as members just u and v:
\forall u \forall v \exists B \forall x (x \in B \iff x = u \lor x = v)
For any two sets a and b, there is a set having whose members are the elements of a or b (or both):
\forall a \forall b \exists B \forall x (x \in B \iff x \in a \lor x \in b)
For any set a, there is a set whose members are exactly the subsets of a:
\forall a \exists B \forall x (x \in B \iff x \subseteq a)
Let x be the set with no members.
We denote x as \varnothing, and call it the empty set.
Number construction
Let S be a function known as the successor function, defined by
S(a) = a \cup \{a\}.
where a is a set.
Then we can construct our numbers by repeatedly applying the successor function to the empty set.
\begin{align*}
0 &= \{\} &=& \varnothing\\
1 &= \{0\} &=& \{\varnothing\}\\
2 &= \{0,1\} &=& \{\varnothing, \{\varnothing\}\}\\
3 &= \{0,1,2\} &=& \{\varnothing, \{\varnothing\},\{\{\varnothing, \{\varnothing\}\}\}\}
\end{align*}