Theorem univ_closed_prod

Proof
01. 1 ⊢ univ U, hypo.
02. 2 ⊢ A ∈ U, hypo.
03. 3 ⊢ B ∈ U, hypo.
04. 1, 2, 3 ⊢ A ∪ B ∈ U, univ_closed_union 1 2 3.
05. 1, 2, 3 ⊢ power (A ∪ B) ∈ U, univ_closed_power 1 4.
06. 1, 2, 3 ⊢ power (power (A ∪ B)) ∈ U, univ_closed_power 1 5.
07. ⊢ A × B ⊆ power (power (A ∪ B)), prod_incl_in_power.
08. 1, 2, 3 ⊢ A × B ∈ U, univ_closed_subset 1 7 6.
univ_closed_prod. ⊢ univ U → A ∈ U → B ∈ U → A × B ∈ U,
  subj_intro_iii 8.

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