Metamath Proof Explorer

Theorem hashbc0

Description: The set of subsets of size zero is the singleton of the empty set. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Hypothesis ramval.c
`|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
Assertion hashbc0
`|- ( A e. V -> ( A C 0 ) = { (/) } )`

Proof

Step Hyp Ref Expression
1 ramval.c
` |-  C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )`
2 0nn0
` |-  0 e. NN0`
3 1 hashbcval
` |-  ( ( A e. V /\ 0 e. NN0 ) -> ( A C 0 ) = { x e. ~P A | ( # ` x ) = 0 } )`
4 2 3 mpan2
` |-  ( A e. V -> ( A C 0 ) = { x e. ~P A | ( # ` x ) = 0 } )`
5 hasheq0
` |-  ( x e. _V -> ( ( # ` x ) = 0 <-> x = (/) ) )`
6 5 elv
` |-  ( ( # ` x ) = 0 <-> x = (/) )`
7 6 anbi2i
` |-  ( ( x e. ~P A /\ ( # ` x ) = 0 ) <-> ( x e. ~P A /\ x = (/) ) )`
8 id
` |-  ( x = (/) -> x = (/) )`
9 0elpw
` |-  (/) e. ~P A`
10 8 9 eqeltrdi
` |-  ( x = (/) -> x e. ~P A )`
11 10 pm4.71ri
` |-  ( x = (/) <-> ( x e. ~P A /\ x = (/) ) )`
12 7 11 bitr4i
` |-  ( ( x e. ~P A /\ ( # ` x ) = 0 ) <-> x = (/) )`
13 12 abbii
` |-  { x | ( x e. ~P A /\ ( # ` x ) = 0 ) } = { x | x = (/) }`
14 df-rab
` |-  { x e. ~P A | ( # ` x ) = 0 } = { x | ( x e. ~P A /\ ( # ` x ) = 0 ) }`
15 df-sn
` |-  { (/) } = { x | x = (/) }`
16 13 14 15 3eqtr4i
` |-  { x e. ~P A | ( # ` x ) = 0 } = { (/) }`
17 4 16 eqtrdi
` |-  ( A e. V -> ( A C 0 ) = { (/) } )`