Theorem choice_on_class

Proof
01. ⊢ ∃f. choice_function f ∧ dom f = UnivCl \ {∅}, choice.
02. 2 ⊢ choice_function f ∧ dom f = UnivCl \ {∅}, hypo.
03. 2 ⊢ choice_function f, conj_eliml 2.
04. 2 ⊢ dom f = UnivCl \ {∅}, conj_elimr 2.
05. 2 ⊢ choice_function (restr f (A \ {∅})), restr_is_choice_fn 3.
06. ⊢ dom (restr f (A \ {∅})) = dom f ∩ (A \ {∅}), dom_restr.
07. 2 ⊢ dom f ∩ (A \ {∅}) = (UnivCl \ {∅}) ∩ (A \ {∅}),
  f_equal 4, f x = x ∩ (A \ {∅}).
08. ⊢ UnivCl ∩ A = A, intersection_neutl.
09. ⊢ A = UnivCl ∩ A, eq_symm 8.
10. ⊢ A \ {∅} = (UnivCl ∩ A) \ {∅}, f_equal 9, f x = x \ {∅}.
11. ⊢ (UnivCl ∩ A) \ {∅} = (UnivCl \ {∅}) ∩ (A \ {∅}), diff_dist_inter.
12. ⊢ A \ {∅} = (UnivCl \ {∅}) ∩ (A \ {∅}), eq_trans 10 11.
13. ⊢ (UnivCl \ {∅}) ∩ (A \ {∅}) = A \ {∅}, eq_symm 12.
14. 2 ⊢ dom f ∩ (A \ {∅}) = A \ {∅}, eq_trans 7 13.
15. 2 ⊢ dom (restr f (A \ {∅})) = A \ {∅}, eq_trans 6 14.
16. 2 ⊢ choice_function (restr f (A \ {∅}))
  ∧ dom (restr f (A \ {∅})) = A \ {∅}, conj_intro 5 15.
17. 2 ⊢ ∃f. choice_function f ∧ dom f = A \ {∅}, ex_intro 16.
choice_on_class. ⊢ ∃f. choice_function f ∧ dom f = A \ {∅}, ex_elim 1 17.

Dependencies
The given proof depends on 10 axioms:
choice, comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.