ZFC estas mallongigo por la aroteorio laŭ Zermelo kaj Fraenkel, kun la aksiomo de elekto (angle choice, france choix).
En la jaro 1908, Ernst Zermelo proponis la Zermelo aroteorio kiel aksiomata matematika bazo. Tamen en la jaro 1925, Abraham Fraenkel skribis leteron al Ernst Zermelo kaj menciis ke ne la kardinala nombro
kaj la aro
(ĉi tie,
estas senfinia aro kaj
signifas
aro de ĉiuj subaroj de
) ne estas konstruebla per lia teorio.
Kun Thoralf Skolem, ili proponis novajn aksiomojn, aldonis la aksiomon de reguleco, kaj anstataŭigis la aksiomon de specifio per la aksiomo de apartigo. Tiu aksiomaro estas konata kiel ZF. Kun la aksiomo de elekto, la aksiomaro nomiĝas ZFE (pli kutime ZFC laŭ la angla aŭ la franca).
Supozu ke
,
, kaj
estas aroj. Per la aksiomo de etendo oni povas difini la koncepton de egaleco de aroj. Unu aro egalas la alian aron se ĉiu elemento ekzistas en ambaŭ aroj:
![{\displaystyle \forall a\forall b[\forall c(c\in a\Leftrightarrow c\in b)\implies a=b]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/eed1d2b0a28c390977ca66500394163c9e99ff28)
Supozu ke
kaj
estas aroj. Per la aksiomo oni povas eldoni elementon de aro se la aro havas pli ol nul elementojn:
![{\displaystyle \forall a(a\neq \varnothing \implies \exists b(b\in a\land b\cap a=\varnothing ))]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/60148c620d2df1ae6f60cd51d3b82c90e09d8a15)
Interesa demando estas kial oni bezonas
en la formulo. La kialo estas la evito de la paradokso de Bertrand Russell.
Supozu ke
,
,
, kaj la finia vico
estas aroj. Cetere supozu ke
estas predikato (petas arojn en rondaj krampoj kiel argumentoj kaj respondas pravon aŭ malpravon).
![{\displaystyle \forall e_{1},\dots ,e_{n}\forall c\exists b\forall a(a\in b\iff [a\in c\land \varphi (a,e_{1},\dots ,e_{n},c)])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d6c977dc9f1cf72c534551e87b951fdd8f90507e)
La ideo de la aksiomo estas ke per la predikato oni povas elekti subaro
de la baza aro
.
Supozu ke
kaj
estas aroj. Oni povas krei superaro de elementoj de
kaj
, nome
:

Supozu ke
,
, kaj
estas aroj. Supozu ke
estas aro de aroj. La aksiomo diras ke oni povas elpreni ĉiu elemento de la aroj de
kaj enmeti ĝin en kuna aro
:
![{\displaystyle \forall k\exists a\forall b\forall c[(c\in b\land b\in k)\implies c\in a]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ca612c2d1da311b390ff577af4f40c275a564891)
La signo
signifas ke akurate nur unu elementon ekzistas. Kontraŭe la signo
signifas ke unu elemento aŭ pli da elementoj ekzistas.
Supozu ke
,
,
,
, kaj
estas aroj. Cetere supozu ke
estas predikato.
![{\displaystyle \forall a\forall e_{1},\dots ,e_{n}[\forall c(c\in a\implies \exists !\,d:\varphi (a,c,e_{1},\dots ,e_{n},d))\implies \exists b\forall c(c\in a\implies \exists d(d\in b\land \varphi (a,c,e_{1},\dots ,e_{n},d)))]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/829947a4785be0292385ab382f900e927ffa6f9d)
La aksiomo enkondukas la ideon de ĵeto. La funkcio
reprezentas ke oni povas ĵeti la nombron 3 al -3 kaj la nombro 42 al -42. Sed oni devas difini la baza aro de la nombroj
kaj
. En la aksiomo oni ne jam povas uzi la koncepton de funkcio sed la ideo estas ke
estas la aro
kaj
estas la aro
. Per
oni povas ĵeti elementojn de
al
.
Ni difinu la mallongigon
kiel
. Supozu ke
,
, kaj
estas aroj
![{\displaystyle \exists a[\exists b(\forall c(c\not \in b)\land b\in a)\land \forall d(d\in a\implies S(d)\in a)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/98b18bf13c0f37cd9b8ddc7ff3d5cddf3af9d542)
Tielmaniere oni povas krei la naturajn nombrojn:
0 |
 |
|
1 |
 |
|
2 |
 |
|
3 |
 |
|
4 |
 |
|
Supozu ke
,
, kaj
estas aroj:

Do por ĉiu subaro
, oni povas enmeti ĉi tiu subaro al
. Tiel oni povas kolekti la tutan aron de subaroj. Fakte oni kutime difinas funkcion
kiu kreas la aro de ĉiuj subaroj (kun la nomo
ĉar alia nomo estas “potencaro”):

Ĉi tiu aksiomo kontribuas la C en ZFC. Supozu ke
kaj
estas aroj kaj
estas predikato:

La aksiomo diras ke, por ĉiu aro kun pli ol unu elemento, oni povas trovi predikaton
kiu elektas elementon de la aro. Se vi havas la aron
kiel
, la predikato
plenumas la kriterion. Ĝenerale por entjeraj finiaj aroj, oni povas difini
. Sed la situacio pri senfinaj aroj estas malfacila kaj oni bezonas la aksiomon de elekto. Pli detale, la aksiomo estas diskutata en aparta artikolo.