Metamath Proof Explorer

Table of Contents - 21.27.20. 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. fences3
51. eqvrelqseqdisj3
52. eqvrelqseqdisj4
53. eqvrelqseqdisj5
54. mainer
55. partimcomember
56. mpet3
57. cpet2
58. cpet
59. mpet
60. mpet2
61. mpets2
62. mpets
63. mainpart
64. fences
65. fences2
66. mainer2
67. mainerim
68. petincnvepres2
69. petincnvepres
70. pet2
71. pet
72. pets
73. dmqsblocks