Proof 01. 1 ⊢ function f, hypo. 02. ⊢ restr f A ⊆ f, restr_is_subclass. 03. 1 ⊢ function (restr f A), function_subclass 2 1. restr_is_function. ⊢ function f → function (restr f A), subj_intro 3.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.