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	|- ( ( A e. Fin /\ B e. A ) -> ( # ` ( A \ { B } ) ) = ( ( # ` A ) - 1 ) )

Proof

Step	Hyp	Ref	Expression
1		snssi	|- ( B e. A -> { B } C_ A )
2		hashssdif	|- ( ( A e. Fin /\ { B } C_ A ) -> ( # ` ( A \ { B } ) ) = ( ( # ` A ) - ( # ` { B } ) ) )
3	1 2	sylan2	|- ( ( A e. Fin /\ B e. A ) -> ( # ` ( A \ { B } ) ) = ( ( # ` A ) - ( # ` { B } ) ) )
4		hashsng	|- ( B e. A -> ( # ` { B } ) = 1 )
5	4	adantl	|- ( ( A e. Fin /\ B e. A ) -> ( # ` { B } ) = 1 )
6	5	oveq2d	|- ( ( A e. Fin /\ B e. A ) -> ( ( # ` A ) - ( # ` { B } ) ) = ( ( # ` A ) - 1 ) )
7	3 6	eqtrd	|- ( ( A e. Fin /\ B e. A ) -> ( # ` ( A \ { B } ) ) = ( ( # ` A ) - 1 ) )