Theorem hash0 14375

Description: The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)

Assertion

Ref	Expression
hash0	⊢ (♯‘∅) = 0

Proof of Theorem hash0

Step	Hyp	Ref	Expression
1		eqid 2734	. 2 ⊢ ∅ = ∅
2		0ex 5275	. . 3 ⊢ ∅ ∈ V
3		hasheq0 14371	. . 3 ⊢ (∅ ∈ V → ((♯‘∅) = 0 ↔ ∅ = ∅))
4	2, 3	ax-mp 5	. 2 ⊢ ((♯‘∅) = 0 ↔ ∅ = ∅)
5	1, 4	mpbir 231	1 ⊢ (♯‘∅) = 0

Syntax hints:   ↔ wb 206   = wceq 1539   ∈ wcel 2107  Vcvv 3457  ∅c0 4306  ‘cfv 6528  0cc0 11122  ♯chash 14338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-cnex 11178  ax-resscn 11179  ax-1cn 11180  ax-icn 11181  ax-addcl 11182  ax-addrcl 11183  ax-mulcl 11184  ax-mulrcl 11185  ax-mulcom 11186  ax-addass 11187  ax-mulass 11188  ax-distr 11189  ax-i2m1 11190  ax-1ne0 11191  ax-1rid 11192  ax-rnegex 11193  ax-rrecex 11194  ax-cnre 11195  ax-pre-lttri 11196  ax-pre-lttrn 11197  ax-pre-ltadd 11198  ax-pre-mulgt0 11199

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-int 4921  df-iun 4967  df-br 5118  df-opab 5180  df-mpt 5200  df-tr 5228  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6288  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7857  df-1st 7983  df-2nd 7984  df-frecs 8275  df-wrecs 8306  df-recs 8380  df-rdg 8419  df-1o 8475  df-er 8714  df-en 8955  df-dom 8956  df-sdom 8957  df-fin 8958  df-card 9946  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268  df-sub 11461  df-neg 11462  df-nn 12234  df-n0 12495  df-z 12582  df-uz 12846  df-fz 13515  df-hash 14339

This theorem is referenced by:  hashrabrsn  14380  hashrabsn01  14381  hashrabsn1  14382  hashge0  14395  elprchashprn2  14404  hash1  14412  hashsn01  14424  hashgt12el  14430  hashgt12el2  14431  hashfzo  14437  hashfzp1  14439  hashxplem  14441  hashmap  14443  hashbc  14461  hashf1lem2  14464  hashf1  14465  hash2pwpr  14484  wrdnfi  14555  lsw0g  14573  ccatlid  14593  ccatrid  14594  rev0  14771  repswsymballbi  14787  fsumconst  15795  incexclem  15841  incexc  15842  fprodconst  15983  sumodd  16394  hashgcdeq  16796  prmreclem4  16926  prmreclem5  16927  0hashbc  17014  ramz2  17031  cshws0  17108  psgnunilem2  19463  psgnunilem4  19465  psgn0fv0  19479  psgnsn  19488  psgnprfval1  19490  efginvrel2  19695  efgredleme  19711  efgcpbllemb  19723  frgpnabllem1  19841  gsumconst  19902  ltbwe  21989  fta1g  26114  fta1  26255  birthdaylem3  26901  ppi1  27112  musum  27139  rpvmasum  27475  umgrislfupgrlem  29035  lfuhgr1v0e  29167  vtxdg0e  29388  vtxdlfgrval  29399  rusgr1vtxlem  29501  wspn0  29840  rusgrnumwwlkl1  29884  rusgr0edg  29889  clwwlknonel  30010  clwwlknon1le1  30016  0ewlk  30029  0wlk  30031  0wlkon  30035  0pth  30040  0clwlk  30045  0crct  30048  0cycl  30049  eupth0  30129  eulerpathpr  30155  wlkl0  30282  f1ocnt  32716  hashxpe  32723  chnub  32930  chnccats1  32933  1arithidom  33489  lvecdim0  33581  fldext2chn  33697  esumcst  34023  cntmeas  34186  ballotlemfval0  34457  signsvtn0  34531  signstfvneq0  34533  signstfveq0  34538  signsvf0  34541  lpadright  34645  derangsn  35121  subfacp1lem6  35136  poimirlem25  37598  poimirlem26  37599  poimirlem27  37600  poimirlem28  37601  unitscyglem4  42140  rp-isfinite6  43474  fzisoeu  45263  upwordnul  46845