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