Axiom of Choice (Premise) Use this premise to introduce the Axiom of Choice at the beginning of a proof. Where: f = family of sets i = index set f(j) = jth element of f c(j) = choice from the jth element of f 1 ALL(f):ALL(i):[Set(f) & Set(i) & EXIST(a):a i & ALL(a):[a f => Set(a) & EXIST(b):b a] & ALL(a):[a i => f(a) f] & ALL(a):[a f => EXIST(b):[b i & a=f(b)]] => EXIST(c):ALL(a):[a i => c(a) f(a)]] Premise