Proof 01. 1 ⊢ A ⊆ B, hypo. 02. 2 ⊢ x ∈ A, hypo. 03. 1, 2 ⊢ x ∈ B, incl_elim 1 2. 04. 1, 2 ⊢ x ∈ A ∩ B, intersection_intro 2 3. 05. 1 ⊢ x ∈ A → x ∈ A ∩ B, subj_intro 4. 06. 1 ⊢ ∀x. x ∈ A → x ∈ A ∩ B, uq_intro 5. 07. 1 ⊢ A ⊆ A ∩ B, incl_intro 6. 08. ⊢ A ∩ B ⊆ A, intersection_incl_left. 09. 1 ⊢ A ∩ B = A, incl_antisym 8 7. intersection_from_incl. ⊢ A ⊆ B → A ∩ B = A, subj_intro 9.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.