Proof
01. 1 ⊢ ∃y. y ∈ M ∧ x ∈ y, hypo.
02. 2 ⊢ y ∈ M ∧ x ∈ y, hypo.
03. 2 ⊢ x ∈ y, conj_elimr 2.
04. 2 ⊢ set x, set_intro 3.
05. 1 ⊢ set x, ex_elim 1 4.
06. 1 ⊢ x ∈ {x | ∃y. y ∈ M ∧ x ∈ y}, comp_intro 5 1.
07. 1 ⊢ x ∈ ⋃M, eq_subst_rev Union_eq 6, P u ↔ x ∈ u.
Union_intro_ex. ⊢ (∃y. y ∈ M ∧ x ∈ y) → x ∈ ⋃M, subj_intro 7.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.