Metamath Proof Explorer


Theorem hashxnn0

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 MVM0*

Proof

Step Hyp Ref Expression
1 hashfxnn0 .:V0*
2 1 a1i MV.:V0*
3 elex MVMV
4 2 3 ffvelrnd MVM0*