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 \mathrm{Fin}\to \left|A\setminus B\right|=\left|A\right|-\left|A\cap B\right|$$

Proof

Step	Hyp	Ref	Expression
1		difin	$$⊢A\setminus \left(A\cap B\right)=A\setminus B$$
2	1	fveq2i	$$⊢\left|A\setminus \left(A\cap B\right)\right|=\left|A\setminus B\right|$$
3		inss1	$$⊢A\cap B\subseteq A$$
4		hashssdif	$$⊢\left(A\in \mathrm{Fin}\wedge A\cap B\subseteq A\right)\to \left|A\setminus \left(A\cap B\right)\right|=\left|A\right|-\left|A\cap B\right|$$
5	3 4	mpan2	$$⊢A\in \mathrm{Fin}\to \left|A\setminus \left(A\cap B\right)\right|=\left|A\right|-\left|A\cap B\right|$$
6	2 5	eqtr3id	$$⊢A\in \mathrm{Fin}\to \left|A\setminus B\right|=\left|A\right|-\left|A\cap B\right|$$