Metamath Proof Explorer

Table of Contents - 21.38.3. Shorter primitive equivalent of ax-groth

1. Grothendieck universes are closed under collection
   1. gru0eld
   2. grusucd
   3. r1rankcld
   4. grur1cld
   5. grurankcld
   6. grurankrcld
   7. cscott
   8. df-scott
   9. scotteqd
   10. scotteq
   11. nfscott
   12. scottabf
   13. scottab
   14. scottabes
   15. scottss
   16. elscottab
   17. scottex2
   18. scotteld
   19. scottelrankd
   20. scottrankd
   21. gruscottcld
   22. ccoll
   23. df-coll
   24. dfcoll2
   25. colleq12d
   26. colleq1
   27. colleq2
   28. nfcoll
   29. collexd
   30. cpcolld
   31. cpcoll2d
   32. grucollcld
2. Minimal universes
   1. ismnu
   2. mnuop123d
   3. mnussd
   4. mnuss2d
   5. mnu0eld
   6. mnuop23d
   7. mnupwd
   8. mnusnd
   9. mnuprssd
   10. mnuprss2d
   11. mnuop3d
   12. mnuprdlem1
   13. mnuprdlem2
   14. mnuprdlem3
   15. mnuprdlem4
   16. mnuprd
   17. mnuunid
   18. mnuund
   19. mnutrcld
   20. mnutrd
   21. mnurndlem1
   22. mnurndlem2
   23. mnurnd
   24. mnugrud
   25. grumnudlem
   26. grumnud
   27. grumnueq
3. Primitive equivalent of ax-groth
   1. expandan
   2. expandexn
   3. expandral
   4. expandrexn
   5. expandrex
   6. expanduniss
   7. ismnuprim
   8. rr-grothprimbi
   9. inagrud
   10. inaex
   11. gruex
   12. rr-groth
   13. rr-grothprim
   14. ismnushort
   15. dfuniv2
   16. rr-grothshortbi
   17. rr-grothshort