x:A. 
y:B. Q(x,y)) 
(f:(A
B). x:A. Q(x,f(x)))x:A. y:B(x). Q(x,y)) (f:(x:AB(x)). x:A. Q(x,f(x)))| Theorem | Name |
| x:A. y:B. Q(x,y)) (f:(AB). x:A. Q(x,f(x))) | [ax_choice_version2] |
| 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] |