Theorem prod_intro

Proof
01. 1 ⊢ x ∈ X, hypo.
02. 2 ⊢ y ∈ Y, hypo.
03. 1, 2 ⊢ x ∈ X ∧ y ∈ Y, conj_intro 1 2.
04. ⊢ (x, y) = (x, y), eq_refl.
05. 1, 2 ⊢ x ∈ X ∧ y ∈ Y ∧ (x, y) = (x, y), conj_intro 3 4.
06. 1, 2 ⊢ ∃b. x ∈ X ∧ b ∈ Y ∧ (x, y) = (x, b), ex_intro 5.
07. 1, 2 ⊢ ∃a. ∃b. a ∈ X ∧ b ∈ Y ∧ (x, y) = (a, b), ex_intro 6.
08. 1 ⊢ set x, set_intro 1.
09. 2 ⊢ set y, set_intro 2.
10. 1, 2 ⊢ set (x, y), set_pair 8 9.
11. 1, 2 ⊢ (x, y) ∈ {t | ∃a. ∃b. a ∈ X ∧ b ∈ Y ∧ t = (a, b)},
  comp_intro 10 7, P u ↔ (∃a. ∃b. a ∈ X ∧ b ∈ Y ∧ u = (a, b)).
12. ⊢ X × Y = {t | ∃a. ∃b. a ∈ X ∧ b ∈ Y ∧ t = (a, b)}, prod_eq.
13. 1, 2 ⊢ (x, y) ∈ X × Y, eq_subst_rev 12 11, P u ↔ (x, y) ∈ u.
prod_intro. ⊢ x ∈ X → y ∈ Y → (x, y) ∈ X × Y, subj_intro_ii 13.

Dependencies
The given proof depends on six axioms:
comp, eq_refl, eq_subst, ext, pairing, union.