Proof 01. 1 ⊢ univ U, hypo. 02. 1 ⊢ ∀I. ∀x. I ∈ U → map x I U → ⋃(img x I) ∈ U, lsubj_conj_elimr univ_equi 1. 03. 1 ⊢ ∀x. I ∈ U → map x I U → ⋃(img x I) ∈ U, uq_elim 2. 04. 1 ⊢ I ∈ U → map x I U → ⋃(img x I) ∈ U, uq_elim 3. univ_closed_family_union. ⊢ univ U → I ∈ U → map x I U → ⋃(img x I) ∈ U, subj_intro 4.