Theorem rng_empty_set

Proof
01. 1 ⊢ y ∈ rng ∅, hypo.
02. 1 ⊢ ∃x. (x, y) ∈ ∅, rng_elim 1.
03. 3 ⊢ (x, y) ∈ ∅, hypo.
04. 3 ⊢ y ∈ ∅, empty_efq 3.
05. 1 ⊢ y ∈ ∅, ex_elim 2 4.
06. ⊢ y ∈ rng ∅ → y ∈ ∅, subj_intro 5.
07. ⊢ ∀y. y ∈ rng ∅ → y ∈ ∅, uq_intro 6.
08. ⊢ rng ∅ ⊆ ∅, incl_intro 7.
09. ⊢ ∅ ⊆ rng ∅, empty_set_is_least.
rng_empty_set. ⊢ rng ∅ = ∅, incl_antisym 8 9.

Dependencies
The given proof depends on four axioms:
comp, efq, eq_subst, ext.