Metamath Proof Explorer
Table of Contents - 5.6.11. The ` # ` (set size) function
- chash
- df-hash
- hashkf
- hashgval
- hashginv
- hashinf
- hashbnd
- hashfxnn0
- hashf
- hashxnn0
- hashresfn
- dmhashres
- hashnn0pnf
- hashnnn0genn0
- hashnemnf
- hashv01gt1
- hashfz1
- hashen
- hasheni
- hasheqf1o
- fiinfnf1o
- focdmex
- hasheqf1oi
- hashf1rn
- hasheqf1od
- fz1eqb
- hashcard
- hashcl
- hashxrcl
- hashclb
- nfile
- hashvnfin
- hashnfinnn0
- isfinite4
- hasheq0
- hashneq0
- hashgt0n0
- hashnncl
- hash0
- hashelne0d
- hashsng
- hashen1
- hash1elsn
- hashrabrsn
- hashrabsn01
- hashrabsn1
- hashfn
- fseq1hash
- hashgadd
- hashgval2
- hashdom
- hashdomi
- hashsdom
- hashun
- hashun2
- hashun3
- hashinfxadd
- hashunx
- hashge0
- hashgt0
- hashge1
- 1elfz0hash
- hashnn0n0nn
- hashunsng
- hashunsngx
- hashunsnggt
- hashprg
- elprchashprn2
- hashprb
- hashprdifel
- prhash2ex
- hashle00
- hashgt0elex
- hashgt0elexb
- hashp1i
- hash1
- hash2
- hash3
- hash4
- pr0hash2ex
- hashss
- prsshashgt1
- hashin
- hashssdif
- hashdif
- hashdifsn
- hashdifpr
- hashsn01
- hashsnle1
- hashsnlei
- hash1snb
- euhash1
- hash1n0
- hashgt12el
- hashgt12el2
- hashgt23el
- hashunlei
- hashsslei
- hashfz
- fzsdom2
- hashfzo
- hashfzo0
- hashfzp1
- hashfz0
- hashxplem
- hashxp
- hashmap
- hashpw
- hashfun
- hashres
- hashreshashfun
- hashimarn
- hashimarni
- resunimafz0
- fnfz0hash
- ffz0hash
- fnfz0hashnn0
- ffzo0hash
- fnfzo0hash
- fnfzo0hashnn0
- hashbclem
- hashbc
- hashfacen
- hashfacenOLD
- hashf1lem1
- hashf1lem1OLD
- hashf1lem2
- hashf1
- hashfac
- leiso
- leisorel
- fz1isolem
- fz1iso
- ishashinf
- seqcoll
- seqcoll2
- phphashd
- phphashrd
- Proper unordered pairs and triples (sets of size 2 and 3)
- hashprlei
- hash2pr
- hash2prde
- hash2exprb
- hash2prb
- prprrab
- nehash2
- hash2prd
- hash2pwpr
- hashle2pr
- hashle2prv
- pr2pwpr
- hashge2el2dif
- hashge2el2difr
- hashge2el2difb
- hashdmpropge2
- hashtplei
- hashtpg
- hashge3el3dif
- elss2prb
- hash2sspr
- exprelprel
- hash3tr
- hash1to3
- Functions with a domain containing at least two different elements
- fundmge2nop0
- fundmge2nop
- fun2dmnop0
- fun2dmnop
- Finite induction on the size of the first component of a binary relation
- hashdifsnp1
- fi1uzind
- brfi1uzind
- brfi1ind
- brfi1indALT
- opfi1uzind
- opfi1ind