Metamath Proof Explorer
Table of Contents - 2.4.28. Finite sets
- dif1enlem
- rexdif1en
- dif1en
- findcard
- findcard2
- findcard2s
- findcard2d
- nnfi
- pssnn
- ssnnfi
- ssnnfiOLD
- 0fin
- unfi
- ssfi
- ssfiALT
- imafi
- pwfir
- pwfilem
- pwfi
- diffi
- cnvfi
- fnfi
- f1oenfi
- f1oenfirn
- f1domfi
- f1domfi2
- enreffi
- ensymfib
- entrfil
- enfii
- enfi
- enfiALT
- domfi
- entrfi
- entrfir
- domtrfil
- domtrfi
- domtrfir
- f1imaenfi
- ssdomfi
- ssdomfi2
- sbthfilem
- sbthfi
- domnsymfi
- sdomdomtrfi
- domsdomtrfi