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 | ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | difin | ⊢ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 ) | |
| 2 | 1 | fveq2i | ⊢ ( ♯ ‘ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) ) = ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) |
| 3 | inss1 | ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 | |
| 4 | hashssdif | ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) | |
| 5 | 3 4 | mpan2 | ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) |
| 6 | 2 5 | eqtr3id | ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) |