Metamath Proof Explorer

Table of Contents - 2.4.34. Finite sets (cont.)

  1. onomeneq
  2. onfin
  3. onfin2
  4. nndomo
  5. nnsdomo
  6. sucdom
  7. snnen2o
  8. 0sdom1dom
  9. 0sdom1domALT
  10. 1sdom2
  11. 1sdom2ALT
  12. sdom1
  13. sdom1OLD
  14. modom
  15. modom2
  16. rex2dom
  17. 1sdom2dom
  18. 1sdom
  19. 1sdomOLD
  20. unxpdomlem1
  21. unxpdomlem2
  22. unxpdomlem3
  23. unxpdom
  24. unxpdom2
  25. sucxpdom
  26. pssinf
  27. fisseneq
  28. ominf
  29. ominfOLD
  30. isinf
  31. isinfOLD
  32. fineqvlem
  33. fineqv
  34. xpfir
  35. ssfid
  36. infi
  37. rabfi
  38. finresfin
  39. f1finf1o
  40. f1finf1oOLD
  41. nfielex
  42. en1eqsn
  43. en1eqsnOLD
  44. en1eqsnbi
  45. dif1ennnALT
  46. enp1ilem
  47. enp1i
  48. enp1iOLD
  49. en2
  50. en3
  51. en4
  52. findcard3
  53. findcard3OLD
  54. ac6sfi
  55. frfi
  56. fimax2g
  57. fimaxg
  58. fisupg
  59. wofi
  60. ordunifi
  61. nnunifi
  62. unblem1
  63. unblem2
  64. unblem3
  65. unblem4
  66. unbnn
  67. unbnn2
  68. isfinite2
  69. nnsdomg
  70. nnsdomgOLD
  71. isfiniteg
  72. infsdomnn
  73. infsdomnnOLD
  74. infn0
  75. infn0ALT
  76. fin2inf
  77. unfilem1
  78. unfilem2
  79. unfilem3
  80. unfir
  81. unfib
  82. unfi2
  83. difinf
  84. fodomfi
  85. fofi
  86. f1fi
  87. imafi
  88. imafiOLD
  89. pwfir
  90. pwfilem
  91. pwfi
  92. xpfi
  93. xpfiOLD
  94. 3xpfi
  95. domunfican
  96. infcntss
  97. prfi
  98. prfiALT
  99. tpfi
  100. fiint
  101. fiintOLD
  102. fodomfir
  103. fodomfib
  104. fodomfiOLD
  105. fodomfibOLD
  106. fofinf1o
  107. rneqdmfinf1o
  108. fidomdm
  109. dmfi
  110. fundmfibi
  111. resfnfinfin
  112. residfi
  113. cnvfiALT
  114. rnfi
  115. f1dmvrnfibi
  116. f1vrnfibi
  117. iunfi
  118. unifi
  119. unifi2
  120. infssuni
  121. unirnffid
  122. mapfi
  123. ixpfi
  124. ixpfi2
  125. mptfi
  126. abrexfi
  127. cnvimamptfin
  128. elfpw
  129. unifpw
  130. f1opwfi
  131. fissuni
  132. fipreima
  133. finsschain
  134. indexfi