Metamath Proof Explorer
Table of Contents - 2.1.14. The empty set
- c0
- df-nul
- dfnul4
- dfnul2
- dfnul3
- dfnul2OLD
- dfnul3OLD
- dfnul4OLD
- noel
- noelOLD
- nel02
- n0i
- ne0i
- ne0d
- n0ii
- ne0ii
- vn0
- vn0ALT
- eq0f
- neq0f
- n0f
- eq0
- eq0ALT
- neq0
- n0
- eq0OLDOLD
- neq0OLD
- n0OLD
- nel0
- reximdva0
- rspn0
- rspn0OLD
- n0rex
- ssn0rex
- n0moeu
- rex0
- reu0
- rmo0
- 0el
- n0el
- eqeuel
- ssdif0
- difn0
- pssdifn0
- pssdif
- ndisj
- difin0ss
- inssdif0
- difid
- difidALT
- dif0
- ab0w
- ab0
- ab0OLD
- ab0ALT
- dfnf5
- ab0orv
- ab0orvALT
- abn0
- abn0OLD
- rab0
- rabeq0w
- rabeq0
- rabn0
- rabxm
- rabnc
- elneldisj
- elnelun
- un0
- in0
- 0un
- 0in
- inv1
- unv
- 0ss
- ss0b
- ss0
- sseq0
- ssn0
- 0dif
- abf
- abfOLD
- eq0rdv
- eq0rdvALT
- csbprc
- csb0
- sbcel12
- sbceqg
- sbceqi
- sbcnel12g
- sbcne12
- sbcel1g
- sbceq1g
- sbcel2
- sbceq2g
- csbcom
- sbcnestgfw
- csbnestgfw
- sbcnestgw
- csbnestgw
- sbcco3gw
- sbcnestgf
- csbnestgf
- sbcnestg
- csbnestg
- sbcco3g
- csbco3g
- csbnest1g
- csbidm
- csbvarg
- csbvargi
- sbccsb
- sbccsb2
- rspcsbela
- sbnfc2
- csbab
- csbun
- csbin
- csbie2df
- 2nreu
- un00
- vss
- 0pss
- npss0
- pssv
- disj
- disjOLD
- disjr
- disj1
- reldisj
- reldisjOLD
- disj3
- disjne
- disjeq0
- disjel
- disj2
- disj4
- ssdisj
- disjpss
- undisj1
- undisj2
- ssindif0
- inelcm
- minel
- undif4
- disjssun
- vdif0
- difrab0eq
- pssnel
- disjdif
- disjdifr
- difin0
- unvdif
- undif1
- undif2
- undifabs
- inundif
- disjdif2
- difun2
- undif
- ssdifin0
- ssdifeq0
- ssundif
- difcom
- pssdifcom1
- pssdifcom2
- difdifdir
- uneqdifeq
- raldifeq
- r19.2z
- r19.2zb
- r19.3rz
- r19.28z
- r19.3rzv
- r19.9rzv
- r19.28zv
- r19.37zv
- r19.45zv
- r19.44zv
- r19.27z
- r19.27zv
- r19.36zv
- ralidmw
- rzal
- rzalALT
- rexn0
- ralidm
- ral0
- ralf0
- rexn0OLD
- ralidmOLD
- ral0OLD
- ralf0OLD
- ralnralall
- falseral0
- raaan
- raaanv
- sbss
- sbcssg
- raaan2
- 2reu4lem
- 2reu4