Axiom of Choice

For any non-empty family of non-empty sets, there exists a choice function
that selects an element from each set in that family.

Version 1  (Non-indexed family of sets)

1	ALL(fam):[Set(fam) & EXIST(a):a ε fam & ALL(a):[a ε fam => Set(a) & EXIST(b):b ε a]
	=> EXIST(choice):ALL(a):[a ε fam => choice(a) ε a]]
	Premise

Version 2  (Indexed family of sets, where i = index set, index = indexing function)

2	ALL(fam):ALL(i):ALL(index):[Set(fam) & Set(i)
	& EXIST(a):a ε fam
	& ALL(a):[a ε fam => Set(a) & EXIST(b):b ε a]
	& ALL(a):[a ε i => index(a) ε fam]
	& ALL(a):[a ε fam => EXIST(b):[b ε i & index(b)=a]]
	=> EXIST(choice):ALL(a):[a ε i => choice(a) ε index(a)]]
	Premise

Version 3  (Indexed family of sets where i = index set)

3	ALL(fam):ALL(i):[Set(fam) & Set(i)
	& EXIST(a):a ε fam
	& ALL(a):[a ε fam => Set(a) & EXIST(b):b ε a]
	& ALL(a):[a ε i => fam(a) ε fam]
	& ALL(a):[a ε fam => EXIST(b):[b ε i & fam(b)=a]]
	=> EXIST(choice):ALL(a):[a ε i => choice(a) ε fam(a)]]
	Premise

Suggestion for families of sets of ordered pairs -- based on version 1 for 
"ordinary" sets above.

4	ALL(fam):[Set(fam) & EXIST(a):a ε fam & ALL(a):[a ε fam => Set'(a) & EXIST(b):EXIST(c):(b,c) ε a]
	=> EXIST(choice):ALL(a):[a ε fam => EXIST(b):EXIST(c):[choice(a)=(b,c) & (b,c) ε a]]]
	Premise