# Metamath Proof Explorer

## Theorem hashbc2

Description: The size of the binomial set is the binomial coefficient. (Contributed by Mario Carneiro, 20-Apr-2015)

Ref Expression
Hypothesis ramval.c
`|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
Assertion hashbc2
`|- ( ( A e. Fin /\ N e. NN0 ) -> ( # ` ( A C N ) ) = ( ( # ` A ) _C N ) )`

### Proof

Step Hyp Ref Expression
1 ramval.c
` |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
2 1 hashbcval
` |-  ( ( A e. Fin /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )`
3 2 fveq2d
` |-  ( ( A e. Fin /\ N e. NN0 ) -> ( # ` ( A C N ) ) = ( # ` { x e. ~P A | ( # ` x ) = N } ) )`
4 nn0z
` |-  ( N e. NN0 -> N e. ZZ )`
5 hashbc
` |-  ( ( A e. Fin /\ N e. ZZ ) -> ( ( # ` A ) _C N ) = ( # ` { x e. ~P A | ( # ` x ) = N } ) )`
6 4 5 sylan2
` |-  ( ( A e. Fin /\ N e. NN0 ) -> ( ( # ` A ) _C N ) = ( # ` { x e. ~P A | ( # ` x ) = N } ) )`
7 3 6 eqtr4d
` |-  ( ( A e. Fin /\ N e. NN0 ) -> ( # ` ( A C N ) ) = ( ( # ` A ) _C N ) )`