Metamath Proof Explorer

Table of Contents - 10.3.15. Left regular elements and domains

1. crlreg
2. cdomn
3. cidom
4. df-rlreg
5. df-domn
6. df-idom
7. rrgval
8. isrrg
9. rrgeq0i
10. rrgeq0
11. rrgsupp
12. rrgss
13. unitrrg
14. rrgnz
15. isdomn
16. domnnzr
17. domnring
18. domneq0
19. domnmuln0
20. isdomn5
21. isdomn2
22. isdomn2OLD
23. domnrrg
24. isdomn6
25. isdomn3
26. isdomn4
27. opprdomnb
28. opprdomn
29. isdomn4r
30. domnlcanb
31. domnlcan
32. domnrcanb
33. domnrcan
34. domneq0r
35. isidom
36. idomdomd
37. idomcringd
38. idomringd