P:Prop. 
P 
P) (A:Type. Finite(A) Unbounded(A))
f:(A
B). Bij(A; B; f)) 
(B ~ A)(x:T. Q(x)) (x:T. Q(x))| Rank | Theorem | Name |
| 4 | P:Prop. P P) (A:Type. Finite(A) Unbounded(A)) | [negnegelim_imp_notfin_imp_unb_inf] |
| cites the following: | ||
| 3 | f:(AB). Bij(A; B; f)) (B ~ A) | [bij_iff_1_1_corr_version2a] |
| 1 | (x:T. Q(x)) (x:T. Q(x)) | [not_over_exists_imp] |