This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )