# Metamath Proof Explorer

## Theorem hashbcval

Description: Value of the "binomial set", the set of all N -element subsets of A . (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 hashbcval
`|- ( ( A e. V /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )`

### Proof

Step Hyp Ref Expression
1 ramval.c
` |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
2 elex
` |-  ( A e. V -> A e. _V )`
3 pwexg
` |-  ( A e. _V -> ~P A e. _V )`
4 3 adantr
` |-  ( ( A e. _V /\ N e. NN0 ) -> ~P A e. _V )`
5 rabexg
` |-  ( ~P A e. _V -> { x e. ~P A | ( # ` x ) = N } e. _V )`
6 4 5 syl
` |-  ( ( A e. _V /\ N e. NN0 ) -> { x e. ~P A | ( # ` x ) = N } e. _V )`
7 fveqeq2
` |-  ( b = x -> ( ( # ` b ) = i <-> ( # ` x ) = i ) )`
8 7 cbvrabv
` |-  { b e. ~P a | ( # ` b ) = i } = { x e. ~P a | ( # ` x ) = i }`
9 simpl
` |-  ( ( a = A /\ i = N ) -> a = A )`
10 9 pweqd
` |-  ( ( a = A /\ i = N ) -> ~P a = ~P A )`
11 simpr
` |-  ( ( a = A /\ i = N ) -> i = N )`
12 11 eqeq2d
` |-  ( ( a = A /\ i = N ) -> ( ( # ` x ) = i <-> ( # ` x ) = N ) )`
13 10 12 rabeqbidv
` |-  ( ( a = A /\ i = N ) -> { x e. ~P a | ( # ` x ) = i } = { x e. ~P A | ( # ` x ) = N } )`
14 8 13 syl5eq
` |-  ( ( a = A /\ i = N ) -> { b e. ~P a | ( # ` b ) = i } = { x e. ~P A | ( # ` x ) = N } )`
15 14 1 ovmpoga
` |-  ( ( A e. _V /\ N e. NN0 /\ { x e. ~P A | ( # ` x ) = N } e. _V ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )`
16 6 15 mpd3an3
` |-  ( ( A e. _V /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )`
17 2 16 sylan
` |-  ( ( A e. V /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )`