Proof 01. 1 ⊢ choice_function f, hypo. 02. 1 ⊢ function f ∧ ∀x. x ∈ dom f → app f x ∈ x, lsubj_elim choice_function_equi 1. 03. 1 ⊢ function f, conj_eliml 2. 04. 1 ⊢ function (restr f A), restr_is_function 3. 06. 1 ⊢ ∀x. x ∈ dom f → app f x ∈ x, conj_elimr 2. 07. 7 ⊢ x ∈ dom (restr f A), hypo. 08. ⊢ dom (restr f A) = dom f ∩ A, dom_restr. 09. 7 ⊢ x ∈ dom f ∩ A, eq_subst 8 7, P u ↔ x ∈ u. 10. 7 ⊢ x ∈ dom f, intersection_eliml 9. 11. 1, 7 ⊢ app f x ∈ x, uq_bounded_elim 6 10. 12. 7 ⊢ x ∈ A, intersection_elimr 9. 13. 1, 7 ⊢ app f x = app (restr f A) x, fn_app_restr 3 10 12. 14. 1, 7 ⊢ app (restr f A) x ∈ x, eq_subst 13 11, P u ↔ u ∈ x. 15. 1 ⊢ x ∈ dom (restr f A) → app (restr f A) x ∈ x, subj_intro 14. 16. 1 ⊢ ∀x. x ∈ dom (restr f A) → app (restr f A) x ∈ x, uq_intro 15. 17. 1 ⊢ choice_function (restr f A), choice_function_intro 4 16. restr_is_choice_fn. ⊢ choice_function f → choice_function (restr f A), subj_intro 17.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.