Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-hash Unicode version

Definition df-hash 11574
 Description: Define the function, which gives the cardinality of a finite set as a member of , and assigns all infinite sets the value . (Contributed by Paul Chapman, 22-Jun-2011.)
Assertion
Ref Expression
df-hash

Detailed syntax breakdown of Definition df-hash
StepHypRef Expression
1 chash 11573 . 2
2 vx . . . . . . 7
3 cvv 2916 . . . . . . 7
42cv 1648 . . . . . . . 8
5 c1 8947 . . . . . . . 8
6 caddc 8949 . . . . . . . 8
74, 5, 6co 6040 . . . . . . 7
82, 3, 7cmpt 4226 . . . . . 6
9 cc0 8946 . . . . . 6
108, 9crdg 6626 . . . . 5
11 com 4804 . . . . 5
1210, 11cres 4839 . . . 4
13 ccrd 7778 . . . 4
1412, 13ccom 4841 . . 3
15 cfn 7068 . . . . 5
163, 15cdif 3277 . . . 4
17 cpnf 9073 . . . . 5
1817csn 3774 . . . 4
1916, 18cxp 4835 . . 3
2014, 19cun 3278 . 2
211, 20wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  hashgval  11576  hashinf  11578  hashf  11580
 Copyright terms: Public domain W3C validator