Metamath Proof Explorer
Table of Contents - 4.1.2. Weak universes
- cwun
- cwunm
- df-wun
- df-wunc
- iswun
- wuntr
- wununi
- wunpw
- wunelss
- wunpr
- wunun
- wuntp
- wunss
- wunin
- wundif
- wunint
- wunsn
- wunsuc
- wun0
- wunr1om
- wunom
- wunfi
- wunop
- wunot
- wunxp
- wunpm
- wunmap
- wunf
- wundm
- wunrn
- wuncnv
- wunres
- wunfv
- wunco
- wuntpos
- intwun
- r1limwun
- r1wunlim
- wunex2
- wunex
- uniwun
- wunex3
- wuncval
- wuncid
- wunccl
- wuncss
- wuncidm
- wuncval2