Metamath Proof Explorer

Table of Contents - 5.7.1. Definitions and basic theorems

1. cword
2. df-word
3. iswrd
4. wrdval
5. iswrdi
6. wrdf
7. wrdfd
8. iswrdb
9. wrddm
10. sswrd
11. snopiswrd
12. wrdexg
13. wrdexb
14. wrdexi
15. wrdsymbcl
16. wrdfn
17. wrdv
18. wrdlndm
19. iswrdsymb
20. wrdfin
21. lencl
22. lennncl
23. wrdffz
24. wrdeq
25. wrdeqi
26. iswrddm0
27. wrd0
28. 0wrd0
29. ffz0iswrd
30. wrdsymb
31. nfwrd
32. csbwrdg
33. wrdnval
34. wrdmap
35. hashwrdn
36. wrdnfi
37. wrdsymb0
38. wrdlenge1n0
39. len0nnbi
40. wrdlenge2n0
41. wrdsymb1
42. wrdlen1
43. fstwrdne
44. fstwrdne0
45. eqwrd
46. elovmpowrd
47. elovmptnn0wrd
48. wrdred1
49. wrdred1hash