Description: The value of the hash function for a set is an extended nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 10-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | hashxnn0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hashfxnn0 | |
|
2 | 1 | a1i | |
3 | elex | |
|
4 | 2 3 | ffvelrnd | |