x:A. B(x) 
B'(x)) 
({x:A| B(x) } ~ {x:A| B'(x) })Thm*
Thm* (
x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) }) Bij(A; B; f)| Rank | Theorem | Name |
| 2 | x:A. B(x) B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) }) | [set_functionality_wrt_one_one_corr_n_pred2] |
| cites the following: | ||
| 1 | Thm*
Thm* ( x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) }) | [card_settype] |
| 0 | [inv_funs_2_identity] | |
| 1 | Bij(A; B; f) | [fun_with_inv2_is_bij] |