Theorem hashdifsn

Description: The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018)

	Ref	Expression
Assertion	hashdifsn	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		snssi	⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 )
2		hashssdif	⊢ ( ( 𝐴 ∈ Fin ∧ { 𝐵 } ⊆ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ { 𝐵 } ) ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ { 𝐵 } ) ) )
4		hashsng	⊢ ( 𝐵 ∈ 𝐴 → ( ♯ ‘ { 𝐵 } ) = 1 )
5	4	adantl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ { 𝐵 } ) = 1 )
6	5	oveq2d	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
7	3 6	eqtrd	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )