Theorem hash0 13729

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 2821	. 2 ⊢ ∅ = ∅
2		0ex 5211	. . 3 ⊢ ∅ ∈ V
3		hasheq0 13725	. . 3 ⊢ (∅ ∈ V → ((♯‘∅) = 0 ↔ ∅ = ∅))
4	2, 3	ax-mp 5	. 2 ⊢ ((♯‘∅) = 0 ↔ ∅ = ∅)
5	1, 4	mpbir 233	1 ⊢ (♯‘∅) = 0

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  Vcvv 3494  ∅c0 4291  ‘cfv 6355  0cc0 10537  ♯chash 13691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-card 9368  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-n0 11899  df-z 11983  df-uz 12245  df-fz 12894  df-hash 13692

This theorem is referenced by:  hashrabrsn  13734  hashrabsn01  13735  hashrabsn1  13736  hashge0  13749  elprchashprn2  13758  hash1  13766  hashsn01  13778  hashgt12el  13784  hashgt12el2  13785  hashfzo  13791  hashfzp1  13793  hashxplem  13795  hashmap  13797  hashbc  13812  hashf1lem2  13815  hashf1  13816  hash2pwpr  13835  wrdnfi  13899  lsw0g  13918  ccatlid  13940  ccatrid  13941  rev0  14126  repswsymballbi  14142  fsumconst  15145  incexclem  15191  incexc  15192  fprodconst  15332  sumodd  15739  hashgcdeq  16126  prmreclem4  16255  prmreclem5  16256  0hashbc  16343  ramz2  16360  cshws0  16435  psgnunilem2  18623  psgnunilem4  18625  psgn0fv0  18639  psgnsn  18648  psgnprfval1  18650  efginvrel2  18853  efgredleme  18869  efgcpbllemb  18881  frgpnabllem1  18993  gsumconst  19054  ltbwe  20253  fta1g  24761  fta1  24897  birthdaylem3  25531  ppi1  25741  musum  25768  rpvmasum  26102  umgrislfupgrlem  26907  lfuhgr1v0e  27036  vtxdg0e  27256  vtxdlfgrval  27267  rusgr1vtxlem  27369  wspn0  27703  rusgrnumwwlkl1  27747  rusgr0edg  27752  clwwlknonel  27874  clwwlknon1le1  27880  0ewlk  27893  0wlk  27895  0wlkon  27899  0pth  27904  0clwlk  27909  0crct  27912  0cycl  27913  eupth0  27993  eulerpathpr  28019  wlkl0  28146  f1ocnt  30525  hashxpe  30529  lvecdim0  31005  esumcst  31322  cntmeas  31485  ballotlemfval0  31753  signsvtn0  31840  signstfvneq0  31842  signstfveq0  31847  signsvf0  31850  lpadright  31955  derangsn  32417  subfacp1lem6  32432  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  rp-isfinite6  39904  fzisoeu  41587