Proof 01. 1 ⊢ x ∈ (A ∩ B) ∩ C, hypo. 02. 1 ⊢ x ∈ A ∩ B, intersection_eliml 1. 03. 1 ⊢ x ∈ A, intersection_eliml 2. 04. 1 ⊢ x ∈ B, intersection_elimr 2. 05. 1 ⊢ x ∈ C, intersection_elimr 1. 06. 1 ⊢ x ∈ B ∩ C, intersection_intro 4 5. 07. 1 ⊢ x ∈ A ∩ (B ∩ C), intersection_intro 3 6. 08. ⊢ x ∈ (A ∩ B) ∩ C → x ∈ A ∩ (B ∩ C), subj_intro 7. 09. 9 ⊢ x ∈ A ∩ (B ∩ C), hypo. 10. 9 ⊢ x ∈ A, intersection_eliml 9. 11. 9 ⊢ x ∈ B ∩ C, intersection_elimr 9. 12. 9 ⊢ x ∈ B, intersection_eliml 11. 13. 9 ⊢ x ∈ C, intersection_elimr 11. 14. 9 ⊢ x ∈ A ∩ B, intersection_intro 10 12. 15. 9 ⊢ x ∈ (A ∩ B) ∩ C, intersection_intro 14 13. 16. ⊢ x ∈ A ∩ (B ∩ C) → x ∈ (A ∩ B) ∩ C, subj_intro 15. 17. ⊢ x ∈ (A ∩ B) ∩ C ↔ x ∈ A ∩ (B ∩ C), bij_intro 8 16. 18. ⊢ ∀x. x ∈ (A ∩ B) ∩ C ↔ x ∈ A ∩ (B ∩ C), uq_intro 17. intersection_assocl. ⊢ (A ∩ B) ∩ C = A ∩ (B ∩ C), ext 18.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.