| Rank | Theorem | Name |
| 6 | Thm* ( a bij a) ~ (a  a) | [nsub_bij_ooc_invpair] |
| cites the following: |
| 5 | Thm*  f:(a bij a). InvFuns(a;a;f; y.least x:. f(x)= y) | [nsub_bij_least_preimage_inverse] |
| 1 | Thm* InvFuns(A;B;f;g)   Bij(A; B; f) | [fun_with_inv2_is_bij] |
| 0 | Thm* InvFuns(A;B;f;g) Surj(A; B; f) | [fun_with_inv2_is_surj] |
| 3 | Thm* f:(a onto b), y:b. (least x:. f(x)=y)  a | [nsub_surj_least_preimage_total] |
| 0 | Thm* InvFuns(A;B;f;g) Inj(A; B; f) | [fun_with_inv2_is_inj] |
| 3 | Thm* f:(a onto b), y:b. f(least x:. f(x)=y) = y | [nsub_surj_least_preimage_works] |
| 0 | Thm* InvFuns(A;B;f;g) InvFuns(A;B;f;h) g = h | [inv_funs_2_unique] |