Theorem dom_empty_set

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

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