Union_intro

Theorem Union_intro

Theorem. Union_intro
y ∈ M → x ∈ y → x ∈ ⋃M

Proof
01. 1 ⊢ y ∈ M, hypo.
02. 2 ⊢ x ∈ y, hypo.
03. 1, 2 ⊢ y ∈ M ∧ x ∈ y, conj_intro 1 2.
04. 1, 2 ⊢ ∃y. y ∈ M ∧ x ∈ y, ex_intro 3.
05. 1, 2 ⊢ x ∈ ⋃M, Union_intro_ex 4.
Union_intro. ⊢ y ∈ M → x ∈ y → x ∈ ⋃M, subj_intro_ii 5.

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