Metamath Proof Explorer
Table of Contents - 3.2. ZFC Set Theory - add the Axiom of Choice
- Introduce the Axiom of Choice
- ax-ac
- zfac
- ac2
- ac3
- ax-ac2
- axac3
- ackm
- axac2
- axac
- axaci
- cardeqv
- numth3
- numth2
- numth
- ac7
- ac7g
- ac4
- ac4c
- ac5
- ac5b
- ac6num
- ac6
- ac6c4
- ac6c5
- ac9
- ac6s
- ac6n
- ac6s2
- ac6s3
- ac6sg
- ac6sf
- ac6s4
- ac6s5
- ac8
- ac9s
- AC equivalents: well-ordering, Zorn's lemma
- numthcor
- weth
- zorn2lem1
- zorn2lem2
- zorn2lem3
- zorn2lem4
- zorn2lem5
- zorn2lem6
- zorn2lem7
- zorn2g
- zorng
- zornn0g
- zorn2
- zorn
- zornn0
- ttukeylem1
- ttukeylem2
- ttukeylem3
- ttukeylem4
- ttukeylem5
- ttukeylem6
- ttukeylem7
- ttukey2g
- ttukeyg
- ttukey
- axdclem
- axdclem2
- axdc
- fodomg
- fodom
- dmct
- rnct
- fodomb
- wdomac
- brdom3
- brdom5
- brdom4
- brdom7disj
- brdom6disj
- fin71ac
- imadomg
- fimact
- fnrndomg
- fnct
- mptct
- iunfo
- iundom2g
- iundomg
- iundom
- unidom
- uniimadom
- uniimadomf
- Cardinal number theorems using Axiom of Choice
- cardval
- cardid
- cardidg
- cardidd
- cardf
- carden
- cardeq0
- unsnen
- carddom
- cardsdom
- domtri
- entric
- entri2
- entri3
- sdomsdomcard
- canth3
- infxpidm
- ondomon
- cardmin
- ficard
- infinf
- unirnfdomd
- konigthlem
- konigth
- alephsucpw
- aleph1
- alephval2
- dominfac
- Cardinal number arithmetic using Axiom of Choice
- iunctb
- unictb
- infmap
- alephadd
- alephmul
- alephexp1
- alephsuc3
- alephexp2
- Cofinality using the Axiom of Choice
- alephreg
- pwcfsdom
- cfpwsdom
- alephom
- smobeth