Metamath Proof Explorer


Table of Contents - 2.4.28. Finite sets

  1. dif1enlem
  2. rexdif1en
  3. dif1en
  4. findcard
  5. findcard2
  6. findcard2s
  7. findcard2d
  8. nnfi
  9. pssnn
  10. ssnnfi
  11. ssnnfiOLD
  12. 0fin
  13. unfi
  14. ssfi
  15. ssfiALT
  16. imafi
  17. pwfir
  18. pwfilem
  19. pwfi
  20. diffi
  21. cnvfi
  22. fnfi
  23. f1oenfi
  24. f1oenfirn
  25. f1domfi
  26. f1domfi2
  27. enreffi
  28. ensymfib
  29. entrfil
  30. enfii
  31. enfi
  32. enfiALT
  33. domfi
  34. entrfi
  35. entrfir
  36. domtrfil
  37. domtrfi
  38. domtrfir
  39. f1imaenfi
  40. ssdomfi
  41. ssdomfi2
  42. sbthfilem
  43. sbthfi
  44. domnsymfi
  45. sdomdomtrfi
  46. domsdomtrfi