Metamath Proof Explorer

Table of Contents - 15.1.1. Definitions and initial properties

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