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. wrdnfiOLD
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