Intersection

Theorem Intersection_elim

Theorem. Intersection_elim
x ∈ ⋂M → y ∈ M → x ∈ y

Proof
01. 1 ⊢ x ∈ ⋂M, hypo.
02. 1 ⊢ x ∈ {x | ∀y. y ∈ M → x ∈ y},
  eq_subst Intersection_eq 1, P A ↔ x ∈ A.
03. 1 ⊢ ∀y. y ∈ M → x ∈ y, comp_elim 2.
04. 1 ⊢ y ∈ M → x ∈ y, uq_elim 3.
Intersection_elim. ⊢ x ∈ ⋂M → y ∈ M → x ∈ y, subj_intro 4.

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