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