Metamath Proof Explorer

Table of Contents - 15.1.1. Definitions and initial properties

1. csur
2. cslt
3. cbday
4. df-no
5. df-slt
6. df-bday
7. elno
8. elnoOLD
9. sltval
10. bdayval
11. nofun
12. nodmon
13. norn
14. nofnbday
15. nodmord
16. elno2
17. elno3
18. sltval2
19. nofv
20. nosgnn0
21. nosgnn0i
22. noreson
23. sltintdifex
24. sltres
25. noxp1o
26. noseponlem
27. nosepon
28. noextend
29. noextendseq
30. noextenddif
31. noextendlt
32. noextendgt
33. nolesgn2o
34. nolesgn2ores
35. nogesgn1o
36. nogesgn1ores