Theorem univ_closed_pair

Proof
01. 1 ⊢ univ U, hypo.
02. 2 ⊢ x ∈ U, hypo.
03. 3 ⊢ y ∈ U, hypo.
04. 1, 2 ⊢ {x} ∈ U, univ_closed_sg 1 2.
05. 1, 2, 3 ⊢ {x, y} ∈ U, univ_closed_pair_set 1 2 3.
06. 1, 2, 3 ⊢ {{x}, {x, y}} ∈ U, univ_closed_pair_set 1 4 5.
07. 1, 2, 3 ⊢ (x, y) ∈ U, eq_subst_rev pair_eq 6, P u ↔ u ∈ U.
univ_closed_pair. ⊢ univ U → x ∈ U → y ∈ U → (x, y) ∈ U,
  subj_intro_iii 7.

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