f:(A
B). Bij(A; B; f)) 
(B ~ A)
(B ~ A)f:(AB). Bij(A; B; f)) (A ~ B)| Rank | Theorem | Name |
| 3 | f:(AB). Bij(A; B; f)) (B ~ A) | [bij_iff_1_1_corr_version2a] |
| cites the following: | ||
| 2 | (B ~ A) | [one_one_corr_2_inversion] |
| 2 | f:(AB). Bij(A; B; f)) (A ~ B) | [bij_iff_1_1_corr_version2] |