Metamath Proof Explorer
Table of Contents - 20.35.3.1. Grothendieck universes are closed under collection
- gru0eld
- grusucd
- r1rankcld
- grur1cld
- grurankcld
- grurankrcld
- cscott
- df-scott
- scotteqd
- scotteq
- nfscott
- scottabf
- scottab
- scottabes
- scottss
- elscottab
- scottex2
- scotteld
- scottelrankd
- scottrankd
- gruscottcld
- ccoll
- df-coll
- dfcoll2
- colleq12d
- colleq1
- colleq2
- nfcoll
- collexd
- cpcolld
- cpcoll2d
- grucollcld