x:A. B(x) ~ B'(x)) 
(x:A. B(x)) ~ (x:A. B'(x))x:A. 
y:B(x). Q(x;y)) (f:(x:A
B(x)). x:A. Q(x;f(x)))| Theorem | Name |
| x:A. B(x) ~ B'(x)) (x:A. B(x)) ~ (x:A. B'(x)) | [one_one_corr_fams_if_one_one_corr_B] |
| cites the following: | |
| x:A. y:B(x). Q(x;y)) (f:(x:AB(x)). x:A. Q(x;f(x))) | [dep_ax_choice_version2] |
| [inv_funs_2_identity] |