Class Difference with Class Difference

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $A$ and $B$ be classes.

Then:

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


Proof

\(\ds \) \(\) \(\ds x \in A \setminus \paren {A \setminus B}\)
\(\ds \) \(\leadstoandfrom\) \(\ds x \in A \land x \notin \paren {A \setminus B}\) Definition of Class Difference
\(\ds \) \(\leadstoandfrom\) \(\ds x \in A \land \lnot \paren {x \in A \land x \notin B}\) Definition of Class Difference
\(\ds \) \(\leadstoandfrom\) \(\ds x \in A \land \paren {x \notin A \lor x \in B}\) De Morgan's Laws
\(\ds \) \(\leadstoandfrom\) \(\ds \paren {x \in A \land x \notin A} \lor \paren {x \in A \land x \in B}\) Conjunction is Left Distributive over Disjunction
\(\ds \) \(\leadstoandfrom\) \(\ds \bot \lor \paren {x \in A \land x \in B}\) Definition of Contradiction
\(\ds \) \(\leadstoandfrom\) \(\ds x \in A \land x \in B\) Disjunction with Contradiction
\(\ds \) \(\leadstoandfrom\) \(\ds x \in \paren {A \cap B}\) Definition of Class Intersection
\(\ds \) \(\leadsto\) \(\ds A \setminus \paren {A \setminus B} = \paren {A \cap B}\) Definition of Class Equality

$\blacksquare$


Also see


Sources