Zermelo-Fraenkel Set Theory

Two sets are equal if and only if they have the same elements:

$\forall A \, \forall B \, [\forall x \, (x \in A \iff x \in B) \implies A = B]$

A set is determined entirely by its elements, not by how it is described.

There exists a set with no elements:

$\exists \emptyset \, \forall x \, (x \notin \emptyset)$

For any two sets $a$ and $b$, there exists a set $\{a, b\}$ whose only elements are $a$ and $b$.

For any set $A$, there exists a set $\bigcup A$ whose elements are exactly the elements of elements of $A$:

$x \in \bigcup A \iff \exists B \, (B \in A \land x \in B)$

For any set $A$, there exists the power set $\mathcal{P}(A) = \{B : B \subseteq A\}$.

There exists an infinite set. Specifically, there exists a set $I$ such that $\emptyset \in I$ and for every $x \in I$, the successor $x \cup \{x\} \in I$. This set contains $\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}, \ldots$, which serves as the construction of $\mathbb{N}$.

For any set $A$ and any property $\phi(x)$ expressible in the language of set theory, there exists the set $\{x \in A : \phi(x)\}$. You can form subsets by filtering with a property, but only subsets of an already-existing set.

If $F$ is a definable function (in the language of set theory) and $A$ is a set, then $\{F(x) : x \in A\}$ is a set. The image of a set under a definable function is a set.

Every nonempty set $A$ contains an element $x$ such that $A \cap x = \emptyset$. This prevents circular membership chains like $a \in b \in a$ and rules out a set being a member of itself.

For any collection of nonempty sets, there exists a function that selects one element from each set. Formally: if $\{A_i\}_{i \in I}$ is a family of nonempty sets, there exists a function $f: I \to \bigcup_{i \in I} A_i$ with $f(i) \in A_i$ for all $i$.