Proof 01. ⊢ C ∪ (A ∩ B) = (C ∪ A) ∩ (C ∪ B), union_distl. 02. ⊢ (A ∩ B) ∪ C = C ∪ (A ∩ B), union_comm. 03. ⊢ (A ∩ B) ∪ C = (C ∪ A) ∩ (C ∪ B), eq_trans 2 1. 04. ⊢ C ∪ A = A ∪ C, union_comm. 05. ⊢ C ∪ B = B ∪ C, union_comm. 06. ⊢ (A ∩ B) ∪ C = (A ∪ C) ∩ (C ∪ B), eq_subst 4 3, P X ↔ (A ∩ B) ∪ C = X ∩ (C ∪ B). union_distr. ⊢ (A ∩ B) ∪ C = (A ∪ C) ∩ (B ∪ C), eq_subst 5 6, P X ↔ (A ∩ B) ∪ C = (A ∪ C) ∩ X.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.