This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashdif

Description: The size of the difference of a finite set and another set is the first set's size minus that of the intersection of both. (Contributed by Steve Rodriguez, 24-Oct-2015)

		Ref	Expression
	Assertion	hashdif	$⊢ A \in Fin \to \|A ∖ B\| = \|A\| - \|A \cap B\|$

Proof

Step	Hyp	Ref	Expression
1		difin	$⊢ A ∖ (A \cap B) = A ∖ B$
2	1	fveq2i	$⊢ \|A ∖ (A \cap B)\| = \|A ∖ B\|$
3		inss1	$⊢ A \cap B \subseteq A$
4		hashssdif	$⊢ (A \in Fin \land A \cap B \subseteq A) \to \|A ∖ (A \cap B)\| = \|A\| - \|A \cap B\|$
5	3 4	mpan2	$⊢ A \in Fin \to \|A ∖ (A \cap B)\| = \|A\| - \|A \cap B\|$
6	2 5	eqtr3id	$⊢ A \in Fin \to \|A ∖ B\| = \|A\| - \|A \cap B\|$