Set Difference is Right Distributive over Set Intersection/Proof 2

From ProofWiki
Jump to navigation Jump to search

Theorem

$\paren {A \cap B} \setminus C = \paren {A \setminus C} \cap \paren {B \setminus C}$


Proof

\(\ds x\) \(\in\) \(\ds \paren {A \cap B} \setminus C\)
\(\ds \leadstoandfrom \ \ \) \(\ds x\) \(\in\) \(\ds A \land x \in B\) Definition of Set Intersection
\(\, \ds \land \, \) \(\ds x\) \(\notin\) \(\ds C\) Definition of Set Difference
\(\ds \leadstoandfrom \ \ \) \(\ds x\) \(\in\) \(\ds A \land x \in B\) Rule of Idempotence
\(\, \ds \land \, \) \(\ds x\) \(\notin\) \(\ds C \land x \notin C\) Rule of Idempotence
\(\ds \leadstoandfrom \ \ \) \(\ds x\) \(\in\) \(\ds A\) Rule of Association
\(\, \ds \land \, \) \(\ds x\) \(\in\) \(\ds x \in B \land x \notin C\)
\(\, \ds \land \, \) \(\ds x\) \(\notin\) \(\ds C\)
\(\ds \leadstoandfrom \ \ \) \(\ds x\) \(\in\) \(\ds A\)
\(\, \ds \land \, \) \(\ds x\) \(\notin\) \(\ds C \land x \in B\) Rule of Commutation
\(\, \ds \land \, \) \(\ds x\) \(\notin\) \(\ds C\)
\(\ds \leadstoandfrom \ \ \) \(\ds x\) \(\in\) \(\ds A \land x \notin C\) Rule of Association
\(\, \ds \land \, \) \(\ds x\) \(\in\) \(\ds B \land x \notin C\)
\(\ds \leadstoandfrom \ \ \) \(\ds x\) \(\in\) \(\ds \paren {A \setminus C}\) Definition of Set Difference
\(\, \ds \land \, \) \(\ds x\) \(\in\) \(\ds \paren {B \setminus C}\) Definition of Set Difference
\(\ds \leadstoandfrom \ \ \) \(\ds x\) \(\in\) \(\ds \paren {A \setminus C} \cap \paren {B \setminus C}\) Definition of Set Intersection

$\blacksquare$