Theorem rng_subclass

Proof
01. 1 ⊢ R ⊆ Q, hypo.
02. 2 ⊢ y ∈ rng R, hypo.
03. 2 ⊢ ∃x. (x, y) ∈ R, rng_elim 2.
04. 4 ⊢ (x, y) ∈ R, hypo.
05. 1, 4 ⊢ (x, y) ∈ Q, incl_elim 1 4.
06. 1, 4 ⊢ y ∈ rng Q, rng_intro 5.
07. 1, 2 ⊢ y ∈ rng Q, ex_elim 3 6.
08. 1 ⊢ y ∈ rng R → y ∈ rng Q, subj_intro 7.
09. 1 ⊢ ∀y. y ∈ rng R → y ∈ rng Q, uq_intro 8.
10. 1 ⊢ rng R ⊆ rng Q, incl_intro 9.
rng_subclass. ⊢ R ⊆ Q → rng R ⊆ rng Q, subj_intro 10.

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