Metamath Proof Explorer

Table of Contents - 2.4.32. Finite sets

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