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