Metamath Proof Explorer

Table of Contents - 2.4.32. Finite sets

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