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 ) = { (/) } )