f:(A
B). Bij(A; B; f)) 
(A ~ B)
f:(AB). Bij(A; B; f) 
(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_version2] |
| cites the following: | ||
| 0 | f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A;B;f;g)) | [bij_imp_exists_inv_version2] |
| 1 | Bij(A; B; f) | [fun_with_inv2_is_bij] |