Theorem function_subclass

Proof
01. 1 ⊢ f ⊆ g, hypo.
02. 2 ⊢ function g, hypo.
03. 2 ⊢ relation g, fn_is_rel 2.
04. 1, 2 ⊢ relation f, relation_subclass 1 3.
05. 5 ⊢ (x, y1) ∈ f, hypo.
06. 6 ⊢ (x, y2) ∈ f, hypo.
07. 1, 5 ⊢ (x, y1) ∈ g, incl_elim 1 5.
08. 1, 6 ⊢ (x, y2) ∈ g, incl_elim 1 6.
09. 1, 2, 5, 6 ⊢ y1 = y2, fn_unique_value 2 7 8.
10. 1, 2, 5 ⊢ (x, y2) ∈ f → y1 = y2, subj_intro 9.
11. 1, 2 ⊢ (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, subj_intro 10.
12. 1, 2 ⊢ ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 11.
13. 1, 2 ⊢ ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 12.
14. 1, 2 ⊢ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_intro 13.
15. 1, 2 ⊢ function f, function_intro 4 14.
function_subclass. ⊢ f ⊆ g → function g → function f, subj_intro_ii 15.