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

Theorem hashen 11967
Description: Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.)
Assertion
Ref Expression
hashen

Proof of Theorem hashen
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fveq2 5708 . . . 4
2 eqid 2489 . . . . . 6
32hashginv 11956 . . . . 5
42hashginv 11956 . . . . 5
53, 4eqeqan12d 2504 . . . 4
61, 5syl5ib 212 . . 3
7 fveq2 5708 . . . 4
82hashgval 11955 . . . . 5
92hashgval 11955 . . . . 5
108, 9eqeqan12d 2504 . . . 4
117, 10syl5ib 212 . . 3
126, 11impbid 185 . 2
13 finnum 8004 . . 3
14 finnum 8004 . . 3
15 carden2 8043 . . 3
1613, 14, 15syl2an 465 . 2
1712, 16bitrd 246 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  =wceq 1670  e.wcel 1732   cvv 3015   class class class wbr 4318  e.cmpt 4376  `'ccnv 4861  domcdm 4862  |`cres 4864  `cfv 5438  (class class class)co 6103   com 6486  reccrdg 6829   cen 7270   cfn 7273   ccrd 7991  0cc0 9161  1c1 9162   caddc 9164   chash 11952
This theorem is referenced by:  hasheni  11968  hasheqf1o  11969  hasheq0  11980  hashsng  11985  hashsdom  11993  hash1snb  12020  euhash1  12021  hash2pr  12027  pr2pwpr  12032  hashxplem  12042  hashmap  12044  hashpw  12045  hashbclem  12052  isercolllem2  12990  isercoll  12992  fz1f1o  13035  summolem3  13039  summolem2a  13040  mertenslem1  13191  hashdvds  13697  crt  13700  phimullem  13701  eulerth  13705  4sqlem11  13863  lagsubg2  15572  orbsta2  15662  dfod2  15809  sylow1lem2  15842  sylow2alem2  15861  sylow2a  15862  slwhash  15867  sylow2  15869  sylow3lem1  15870  cyggenod  16104  lt6abl  16114  gsumval3  16124  ablfac1c  16244  ablfac1eu  16246  ablfaclem3  16260  fta1blem  21106  vieta1  21244  basellem5  21888  isppw  21918  eupai  22710  derangen2  26208  subfacp1lem3  26216  subfacp1lem5  26218  erdsze2lem1  26237  erdsze2lem2  26238  prodmolem3  26598  prodmolem2a  26599  bpolylem  27433  eldioph2lem1  28246  frlmpwfi  28602  isnumbasgrplem3  28610  idomsubgmo  28745  hash3tr  29415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382  ax-cnex 9217  ax-resscn 9218  ax-1cn 9219  ax-icn 9220  ax-addcl 9221  ax-addrcl 9222  ax-mulcl 9223  ax-mulrcl 9224  ax-mulcom 9225  ax-addass 9226  ax-mulass 9227  ax-distr 9228  ax-i2m1 9229  ax-1ne0 9230  ax-1rid 9231  ax-rnegex 9232  ax-rrecex 9233  ax-cnre 9234  ax-pre-lttri 9235  ax-pre-lttrn 9236  ax-pre-ltadd 9237  ax-pre-mulgt0 9238
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-nel 2655  df-ral 2764  df-rex 2765  df-reu 2766  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-int 4155  df-iun 4199  df-br 4319  df-opab 4377  df-mpt 4378  df-tr 4412  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-riota 6062  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-om 6487  df-recs 6795  df-rdg 6830  df-er 7067  df-en 7274  df-dom 7275  df-sdom 7276  df-fin 7277  df-card 7995  df-pnf 9299  df-mnf 9300  df-xr 9301  df-ltxr 9302  df-le 9303  df-sub 9474  df-neg 9475  df-nn 10189  df-n0 10446  df-z 10511  df-uz 10726  df-hash 11953
  Copyright terms: Public domain W3C validator