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 Fin A B = A A B

Proof

Step Hyp Ref Expression
1 difin A A B = A B
2 1 fveq2i A A B = A B
3 inss1 A B A
4 hashssdif A Fin A B A A A B = A A B
5 3 4 mpan2 A Fin A A B = A A B
6 2 5 eqtr3id A Fin A B = A A B