Theorem Intersection_intro_witness

Proof
01. 1 ⊢ y ∈ M, hypo.
02. 2 ⊢ ∀y. y ∈ M → x ∈ y, hypo.
03. 2 ⊢ y ∈ M → x ∈ y, uq_elim 2.
04. 1, 2 ⊢ x ∈ y, subj_elim 3 1.
05. 1, 2 ⊢ set x, set_intro 4.
06. 1, 2 ⊢ x ∈ ⋂M, Intersection_intro 5 2.
Intersection_intro_witness. ⊢ y ∈ M →
  (∀y. y ∈ M → x ∈ y) → x ∈ ⋂M, subj_intro_ii 6.

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