Proof 01. ⊢ (A ∩ B) \ C = (A ∩ B) ∩ compl C, diff_as_inter. 02. ⊢ compl C ∩ compl C = compl C, intersection_idem. 03. ⊢ compl C = compl C ∩ compl C, eq_symm 2. 04. ⊢ (A ∩ B) ∩ compl C = (A ∩ B) ∩ (compl C ∩ compl C), f_equal 3, f x = (A ∩ B) ∩ x. 05. ⊢ (A ∩ B) ∩ (compl C ∩ compl C) = ((A ∩ B) ∩ compl C) ∩ compl C, intersection_assocr. 06. ⊢ (A ∩ B) ∩ compl C = compl C ∩ (A ∩ B), intersection_comm. 07. ⊢ compl C ∩ (A ∩ B) = (compl C ∩ A) ∩ B, intersection_assocr. 08. ⊢ (A ∩ B) ∩ compl C = (compl C ∩ A) ∩ B, eq_trans 6 7. 09. ⊢ compl C ∩ A = A ∩ compl C, intersection_comm. 10. ⊢ A \ C = A ∩ compl C, diff_as_inter. 11. ⊢ A ∩ compl C = A \ C, eq_symm 10. 12. ⊢ compl C ∩ A = A \ C, eq_trans 9 11. 13. ⊢ (A ∩ B) ∩ compl C = (A \ C) ∩ B, eq_subst 12 8, P x ↔ (A ∩ B) ∩ compl C = x ∩ B. 14. ⊢ (A ∩ B) ∩ compl C = ((A ∩ B) ∩ compl C) ∩ compl C, eq_trans 4 5. 15. ⊢ (A ∩ B) ∩ compl C = (A \ C) ∩ B ∩ compl C, eq_subst 13 14, P x ↔ (A ∩ B) ∩ compl C = x ∩ compl C. 16. ⊢ (A \ C) ∩ B ∩ compl C = (A \ C) ∩ (B ∩ compl C), intersection_assocl. 17. ⊢ (A ∩ B) ∩ compl C = (A \ C) ∩ (B ∩ compl C), eq_trans 15 16. 18. ⊢ B \ C = B ∩ compl C, diff_as_inter. 19. ⊢ (A ∩ B) ∩ compl C = (A \ C) ∩ (B \ C), eq_subst_rev 18 17, P x ↔ (A ∩ B) ∩ compl C = (A \ C) ∩ x. diff_dist_inter. ⊢ (A ∩ B) \ C = (A \ C) ∩ (B \ C), eq_trans 1 19.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.