Theorem univ_closed_pair_set

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, 3 ⊢ {y} ∈ U, univ_closed_sg 1 3.
06. 1, 2, 3 ⊢ {x, y} ∈ U, univ_closed_union 1 4 5.
univ_closed_pair_set. ⊢ univ U → x ∈ U → y ∈ U → {x, y} ∈ U,
  subj_intro_iii 6.

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