Theorem inv_img_incl

Proof
01. 1 ⊢ A ⊆ B, hypo.
02. 1 ⊢ A ∪ B = B, union_from_incl 1.
03. 1 ⊢ inv_img R (A ∪ B) = inv_img R B, f_equal 2, f u = inv_img R u.
04. ⊢ inv_img R A ∪ inv_img R B = inv_img R (A ∪ B),
  eq_symm inv_img_dist_union.
05. 1 ⊢ inv_img R A ∪ inv_img R B = inv_img R B, eq_trans 4 3.
06. 1 ⊢ inv_img R A ⊆ inv_img R B, incl_from_union 5.
inv_img_incl. ⊢ A ⊆ B → inv_img R A ⊆ inv_img R B, subj_intro 6.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.