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

Definition df-hash 12406
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 12405 . 2
2 vx . . . . . . 7
3 cvv 3109 . . . . . . 7
42cv 1394 . . . . . . . 8
5 c1 9514 . . . . . . . 8
6 caddc 9516 . . . . . . . 8
74, 5, 6co 6296 . . . . . . 7
82, 3, 7cmpt 4510 . . . . . 6
9 cc0 9513 . . . . . 6
108, 9crdg 7094 . . . . 5
11 com 6700 . . . . 5
1210, 11cres 5006 . . . 4
13 ccrd 8337 . . . 4
1412, 13ccom 5008 . . 3
15 cfn 7536 . . . . 5
163, 15cdif 3472 . . . 4
17 cpnf 9646 . . . . 5
1817csn 4029 . . . 4
1916, 18cxp 5002 . . 3
2014, 19cun 3473 . 2
211, 20wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  hashgval  12408  hashinf  12410  hashf  12412
  Copyright terms: Public domain W3C validator