Proof 01. 1 ⊢ x ∈ A ∩ B, hypo. 02. 1 ⊢ x ∈ A ∧ x ∈ B, intersection_elim 1. 03. 1 ⊢ x ∈ A, conj_eliml 2. 04. ⊢ x ∈ A ∩ B → x ∈ A, subj_intro 3. 05. ⊢ ∀x. x ∈ A ∩ B → x ∈ A, uq_intro 4. intersection_incl_left. ⊢ A ∩ B ⊆ A, incl_intro 5.
Dependencies
The given proof depends on two axioms:
comp, eq_subst.