f is 1-1 corr
f:(A
B). Bij(A; B; f) 
(
g:(BA). InvFuns(A;B;f;g)) Bij(A; B; f)| Rank | Theorem | Name |
| 2 | f is 1-1 corr | [bij_iff_is_1_1_corr] |
| cites the following: | ||
| 0 | f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A;B;f;g)) | [bij_imp_exists_inv2] |
| 1 | Bij(A; B; f) | [fun_with_inv2_is_bij] |