Theorem univ_closed_Union

Proof
01. 1 ⊢ univ U, hypo.
02. 2 ⊢ M ∈ U, hypo.
03. ⊢ map (id M) M M, id_is_map.
04. 1, 2 ⊢ M ⊆ U, univ_trans 1 2.
05. 1, 2 ⊢ map (id M) M U, map_rng_weaken 3 4.
06. 1, 2 ⊢ ⋃(img (id M) M) ∈ U, univ_closed_family_union 1 2 5.
07. ⊢ M ⊆ M, incl_refl.
08. ⊢ img (id M) M = M, id_img 7.
09. 1, 2 ⊢ ⋃M ∈ U, eq_subst 8 6, P x ↔ ⋃x ∈ U.
univ_closed_Union. ⊢ univ U → M ∈ U → ⋃M ∈ U, subj_intro_ii 9.

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