Theorem prod_elim_lemma

Proof
01. 1 ⊢ t ∈ X × Y, hypo.
02. 1 ⊢ ∃x. ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y), prod_elim 1.
03. 3 ⊢ ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y), hypo.
04. 4 ⊢ x ∈ X ∧ y ∈ Y ∧ t = (x, y), hypo.
05. 4 ⊢ x ∈ X ∧ y ∈ Y, conj_eliml 4.
06. 4 ⊢ x ∈ X, conj_eliml 5.
07. 4 ⊢ y ∈ Y, conj_elimr 5.
08. 4 ⊢ t = (x, y), conj_elimr 4.
09. 4 ⊢ set x, set_intro 6.
10. 4 ⊢ set y, set_intro 7.
11. 4 ⊢ fst (x, y) = x, pair_fst 9 10.
12. 4 ⊢ scd (x, y) = y, pair_scd 9 10.
13. 4 ⊢ fst t = x, eq_subst_rev 8 11, P u ↔ fst u = x.
14. 4 ⊢ scd t = y, eq_subst_rev 8 12, P u ↔ scd u = y.
15. 4 ⊢ fst t ∈ X ∧ y ∈ Y, eq_subst_rev 13 5.
16. 4 ⊢ fst t ∈ X ∧ scd t ∈ Y, eq_subst_rev 14 15.
17. 3 ⊢ fst t ∈ X ∧ scd t ∈ Y, ex_elim 3 16.
18. 1 ⊢ fst t ∈ X ∧ scd t ∈ Y, ex_elim 2 17.
prod_elim_lemma. ⊢ t ∈ X × Y → fst t ∈ X ∧ scd t ∈ Y, subj_intro 18.

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