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. ssnnfiOLD
16. 0fin
17. unfi
18. ssfi
19. ssfiALT
20. imafi
21. pwfir
22. pwfilem
23. pwfi
24. diffi
25. cnvfi
26. fnfi
27. f1oenfi
28. f1oenfirn
29. f1domfi
30. f1domfi2
31. enreffi
32. ensymfib
33. entrfil
34. enfii
35. enfi
36. enfiALT
37. domfi
38. entrfi
39. entrfir
40. domtrfil
41. domtrfi
42. domtrfir
43. f1imaenfi
44. ssdomfi
45. ssdomfi2
46. sbthfilem
47. sbthfi
48. domnsymfi
49. sdomdomtrfi
50. domsdomtrfi
51. sucdom2