Metamath Proof Explorer
Table of Contents - 2.1.20. The intersection of a class
- cint
- df-int
- dfint2
- inteq
- inteqi
- inteqd
- elint
- elint2
- elintg
- elinti
- nfint
- elintab
- elintrab
- elintrabg
- int0
- intss1
- ssint
- ssintab
- ssintub
- ssmin
- intmin
- intss
- intssuni
- ssintrab
- unissint
- intssuni2
- intminss
- intmin2
- intmin3
- intmin4
- intab
- int0el
- intun
- intprg
- intpr
- intprOLD
- intprgOLD
- intsng
- intsn
- uniintsn
- uniintab
- intunsn
- rint0
- elrint
- elrint2