Proof 01. 1 ⊢ A ∩ B = A, hypo. 02. 2 ⊢ x ∈ A, hypo. 03. 1, 2 ⊢ x ∈ A ∩ B, eq_subst_rev 1 2, P u ↔ x ∈ u. 04. 1, 2 ⊢ x ∈ B, intersection_elimr 3. 05. 1 ⊢ x ∈ A → x ∈ B, subj_intro 4. 06. 1 ⊢ ∀x. x ∈ A → x ∈ B, uq_intro 5. 07. 1 ⊢ A ⊆ B, incl_intro 6. incl_from_intersection. ⊢ A ∩ B = A → A ⊆ B, subj_intro 7.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.