Metamath Proof Explorer

Table of Contents - 21.27.22. Partition-Equivalence Theorems

1. disjim
2. disjimi
3. detlem
4. eldisjim
5. eldisjim2
6. eqvrel0
7. det0
8. eqvrelcoss0
9. eqvrelid
10. eqvrel1cossidres
11. eqvrel1cossinidres
12. eqvrel1cossxrnidres
13. detid
14. eqvrelcossid
15. detidres
16. detinidres
17. detxrnidres
18. disjlem14
19. disjlem17
20. disjlem18
21. disjlem19
22. disjdmqsss
23. disjdmqscossss
24. disjdmqs
25. disjdmqseq
26. eldisjn0el
27. partim2
28. partim
29. partimeq
30. eldisjlem19
31. membpartlem19
32. petlem
33. petlemi
34. pet02
35. pet0
36. petid2
37. petid
38. petidres2
39. petidres
40. petinidres2
41. petinidres
42. petxrnidres2
43. petxrnidres
44. eqvreldisj1
45. eqvreldisj2
46. eqvreldisj3
47. eqvreldisj4
48. eqvreldisj5
49. eqvrelqseqdisj2
50. disjimeldisjdmqs
51. eldisjsim1
52. eldisjsim2
53. disjsssrels
54. eldisjsim3
55. eldisjsim4
56. eldisjsim5
57. eldisjs6
58. eldisjs7
59. dfdisjs6
60. dfdisjs7
61. fences3
62. eqvrelqseqdisj3
63. eqvrelqseqdisj4
64. eqvrelqseqdisj5
65. mainer
66. partimcomember
67. mpet3
68. cpet2
69. cpet
70. mpet
71. mpet2
72. mpets2
73. mpets
74. mainpart
75. fences
76. fences2
77. mainer2
78. mainerim
79. petincnvepres2
80. petincnvepres
81. pet2
82. pet
83. pets
84. dmqsblocks