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 e. Fin -> ( # ` ( A \ B ) ) = ( ( # ` A ) - ( # ` ( A i^i B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		difin	|- ( A \ ( A i^i B ) ) = ( A \ B )
2	1	fveq2i	|- ( # ` ( A \ ( A i^i B ) ) ) = ( # ` ( A \ B ) )
3		inss1	|- ( A i^i B ) C_ A
4		hashssdif	|- ( ( A e. Fin /\ ( A i^i B ) C_ A ) -> ( # ` ( A \ ( A i^i B ) ) ) = ( ( # ` A ) - ( # ` ( A i^i B ) ) ) )
5	3 4	mpan2	|- ( A e. Fin -> ( # ` ( A \ ( A i^i B ) ) ) = ( ( # ` A ) - ( # ` ( A i^i B ) ) ) )
6	2 5	eqtr3id	|- ( A e. Fin -> ( # ` ( A \ B ) ) = ( ( # ` A ) - ( # ` ( A i^i B ) ) ) )