Theorem prod_elim

Proof
01. 1 ⊢ t ∈ X × Y, hypo.
02. ⊢ X × Y = {t | ∃x. ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y)}, prod_eq.
03. 1 ⊢ t ∈ {t | ∃x. ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y)},
  eq_subst 2 1, P u ↔ t ∈ u.
04. 1 ⊢ ∃x. ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y), comp_elim 3.
prod_elim. ⊢ t ∈ X × Y → ∃x. ∃y. x ∈ X ∧ y ∈ Y ∧ t = (x, y),
  subj_intro 4.

Dependencies
The given proof depends on two axioms:
comp, eq_subst.