Intersection

Theorem Intersection_intro

Theorem. Intersection_intro
set x → (∀y. y ∈ M → x ∈ y) → x ∈ ⋂M

Proof
01. 1 ⊢ set x, hypo.
02. 2 ⊢ ∀y. y ∈ M → x ∈ y, hypo.
03. 1, 2 ⊢ x ∈ {x | ∀y. y ∈ M → x ∈ y}, comp_intro 1 2.
04. 1, 2 ⊢ x ∈ ⋂M, eq_subst_rev Intersection_eq 3, P A ↔ x ∈ A.
Intersection_intro. ⊢ set x → (∀y. y ∈ M → x ∈ y) → x ∈ ⋂M,
  subj_intro_ii 4.

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