Proof 01. 1 ⊢ function f, hypo. 02. 2 ⊢ ∀x. x ∈ dom f → app f x ∈ x, hypo. 03. 1, 2 ⊢ function f ∧ ∀x. x ∈ dom f → app f x ∈ x, conj_intro 1 2. 04. 1, 2 ⊢ choice_function f, rsubj_elim choice_function_equi 3. choice_function_intro. ⊢ function f → (∀x. x ∈ dom f → app f x ∈ x) → choice_function f, subj_intro_ii 4.