Theorem prod_elim_pair

Proof
01. 1 ⊢ (x, y) ∈ X × Y, hypo.
02. 1 ⊢ ∃a. ∃b. a ∈ X ∧ b ∈ Y ∧ (x, y) = (a, b), prod_elim 1.
03. 3 ⊢ ∃b. a ∈ X ∧ b ∈ Y ∧ (x, y) = (a, b), hypo.
04. 4 ⊢ a ∈ X ∧ b ∈ Y ∧ (x, y) = (a, b), hypo.
05. 4 ⊢ a ∈ X ∧ b ∈ Y, conj_eliml 4.
06. 4 ⊢ (x, y) = (a, b), conj_elimr 4.
07. 1 ⊢ set (x, y), set_intro 1.
08. 1 ⊢ set x, setl_from_pair 7.
09. 1 ⊢ set y, setr_from_pair 7.
10. 1 ⊢ set x ∧ set y, conj_intro 8 9.
11. 1, 4 ⊢ x = a ∧ y = b, pair_property_conj 10 6.
12. 1, 4 ⊢ x = a, conj_eliml 11.
13. 1, 4 ⊢ y = b, conj_elimr 11.
14. 1, 4 ⊢ x ∈ X ∧ b ∈ Y, eq_subst_rev 12 5.
15. 1, 4 ⊢ x ∈ X ∧ y ∈ Y, eq_subst_rev 13 14.
16. 1, 3 ⊢ x ∈ X ∧ y ∈ Y, ex_elim 3 15.
17. 1 ⊢ x ∈ X ∧ y ∈ Y, ex_elim 2 16.
prod_elim_pair. ⊢ (x, y) ∈ X × Y → x ∈ X ∧ y ∈ Y, subj_intro 17.

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