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. 0finOLD
13. unfi
14. unfid
15. ssfi
16. ssfiALT
17. diffi
18. cnvfi
19. pwssfi
20. fnfi
21. f1oenfi
22. f1oenfirn
23. f1domfi
24. f1domfi2
25. enreffi
26. ensymfib
27. entrfil
28. enfii
29. enfi
30. enfiALT
31. domfi
32. entrfi
33. entrfir
34. domtrfil
35. domtrfi
36. domtrfir
37. f1imaenfi
38. ssdomfi
39. ssdomfi2
40. sbthfilem
41. sbthfi
42. domnsymfi
43. sdomdomtrfi
44. domsdomtrfi
45. sucdom2