f:(A
B). Bij(A; B; f)) 
(A ~~ B)
f:(AB). Bij(A; B; f) 
(g:(BA). InvFuns(A; B; f; g))f:(AB), g:(BA). InvFuns(A; B; f; g) Bij(A; B; f)| Rank | Theorem | Name |
| 2 | f:(AB). Bij(A; B; f)) (A ~~ B) | [bij_iff_1_1_corr] |
| cites the following: | ||
| 1 | f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A; B; f; g)) | [bij_imp_exists_inv] |
| 0 | f:(AB), g:(BA). InvFuns(A; B; f; g) Bij(A; B; f) | [fun_with_inv_is_bij] |