Proof 01. 1 ⊢ x ∈ A ∩ (B ∪ C), hypo. 02. 1 ⊢ x ∈ A, intersection_eliml 1. 03. 1 ⊢ x ∈ B ∪ C, intersection_elimr 1. 04. 1 ⊢ x ∈ B ∨ x ∈ C, union_elim 3. 05. 5 ⊢ x ∈ B, hypo. 06. 1, 5 ⊢ x ∈ A ∩ B, intersection_intro 2 5. 07. 1, 5 ⊢ x ∈ (A ∩ B) ∪ (A ∩ C), union_introl 6. 08. 8 ⊢ x ∈ C, hypo. 09. 1, 8 ⊢ x ∈ A ∩ C, intersection_intro 2 8. 10. 1, 8 ⊢ x ∈ (A ∩ B) ∪ (A ∩ C), union_intror 9. 11. 1 ⊢ x ∈ (A ∩ B) ∪ (A ∩ C), disj_elim 4 7 10. 12. ⊢ x ∈ A ∩ (B ∪ C) → x ∈ (A ∩ B) ∪ (A ∩ C), subj_intro 11. 13. 13 ⊢ x ∈ (A ∩ B) ∪ (A ∩ C), hypo. 14. 13 ⊢ x ∈ A ∩ B ∨ x ∈ A ∩ C, union_elim 13. 15. 15 ⊢ x ∈ A ∩ B, hypo. 16. 15 ⊢ x ∈ A, intersection_eliml 15. 17. 15 ⊢ x ∈ B, intersection_elimr 15. 18. 15 ⊢ x ∈ B ∪ C, union_introl 17. 19. 15 ⊢ x ∈ A ∩ (B ∪ C), intersection_intro 16 18. 20. 20 ⊢ x ∈ A ∩ C, hypo. 21. 20 ⊢ x ∈ A, intersection_eliml 20. 22. 20 ⊢ x ∈ C, intersection_elimr 20. 23. 20 ⊢ x ∈ B ∪ C, union_intror 22. 24. 20 ⊢ x ∈ A ∩ (B ∪ C), intersection_intro 21 23. 25. 13 ⊢ x ∈ A ∩ (B ∪ C), disj_elim 14 19 24. 26. ⊢ x ∈ (A ∩ B) ∪ (A ∩ C) → x ∈ A ∩ (B ∪ C), subj_intro 25. 27. ⊢ x ∈ A ∩ (B ∪ C) ↔ x ∈ (A ∩ B) ∪ (A ∩ C), bij_intro 12 26. 28. ⊢ ∀x. x ∈ A ∩ (B ∪ C) ↔ x ∈ (A ∩ B) ∪ (A ∩ C), uq_intro 27. intersection_distl. ⊢ A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C), ext 28.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.