Union_elim

Theorem Union_elim

Theorem. Union_elim
x ∈ ⋃M → ∃y. y ∈ M ∧ x ∈ y

Proof
01. 1 ⊢ x ∈ ⋃M, hypo.
02. 1 ⊢ x ∈ {x | ∃y. y ∈ M ∧ x ∈ y}, eq_subst Union_eq 1, P u ↔ x ∈ u.
03. 1 ⊢ ∃y. y ∈ M ∧ x ∈ y, comp_elim 2.
Union_elim. ⊢ x ∈ ⋃M → ∃y. y ∈ M ∧ x ∈ y, subj_intro 3.

Dependencies
The given proof depends on two axioms:
comp, eq_subst.