Hereditarily finite set

Set

definiendum $V_\omega$ in it
postulate $\emptyset\in V_\omega$
for all $x\in V_\omega$
postulate ${\mathcal P}(x)\in V_\omega $
postulate $x = \emptyset\ \lor\ \exists (y\in V_\omega).\ x = {\mathcal P}(y) $

Discussion

Idea

This is the set of all finite sets constructable when starting with $\emptyset$. It's the smallest infinite Grothendieck universe, as well as a model of ZFC.

Reference

Wikipedia: Hereditarily finite set


Requirements

Power set, Empty set

Element of

Grothendieck universe

Set universe