Proof
01. 1 ⊢ (x, y) ∈ R, hypo.
02. 1 ⊢ set (x, y), set_intro 1.
03. 1 ⊢ set x, setl_from_pair 2.
04. 1 ⊢ ∃y. (x, y) ∈ R, ex_intro 1.
05. 1 ⊢ x ∈ {x | ∃y. (x, y) ∈ R}, comp_intro 3 4.
06. 1 ⊢ x ∈ dom R, eq_subst_rev dom_eq 5, P u ↔ x ∈ u.
dom_intro. ⊢ (x, y) ∈ R → x ∈ dom R, subj_intro 6.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.