Theorem intersection_eliml

Theorem. intersection_eliml
x ∈ A ∩ B → x ∈ A
Proof
01. 1 ⊢ x ∈ A ∩ B, hypo.
02. 1 ⊢ x ∈ A ∧ x ∈ B, intersection_elim 1.
03. 1 ⊢ x ∈ A, conj_eliml 2.
intersection_eliml. ⊢ x ∈ A ∩ B → x ∈ A, subj_intro 3.

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