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

Theorem hashen 11910
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 5685 . . . 4
2 eqid 2481 . . . . . 6
32hashginv 11899 . . . . 5
42hashginv 11899 . . . . 5
53, 4eqeqan12d 2496 . . . 4
61, 5syl5ib 212 . . 3
7 fveq2 5685 . . . 4
82hashgval 11898 . . . . 5
92hashgval 11898 . . . . 5
108, 9eqeqan12d 2496 . . . 4
117, 10syl5ib 212 . . 3
126, 11impbid 185 . 2
13 finnum 7949 . . 3
14 finnum 7949 . . 3
15 carden2 7988 . . 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 1662  e.wcel 1724   cvv 3006   class class class wbr 4302  e.cmpt 4360  `'ccnv 4843  domcdm 4844  |`cres 4846  `cfv 5417  (class class class)co 6067   com 6441  reccrdg 6779   cen 7218   cfn 7221   ccrd 7936  0cc0 9104  1c1 9105   caddc 9107   chash 11895
This theorem is referenced by:  hasheni  11911  hasheqf1o  11912  hasheq0  11923  hashsng  11928  hashsdom  11936  hash1snb  11963  euhash1  11964  hash2pr  11970  hashxplem  11982  hashmap  11984  hashpw  11985  hashbclem  11992  isercolllem2  12929  isercoll  12931  fz1f1o  12974  summolem3  12978  summolem2a  12979  mertenslem1  13130  hashdvds  13636  crt  13639  phimullem  13640  eulerth  13644  4sqlem11  13802  lagsubg2  15504  orbsta2  15594  dfod2  15703  sylow1lem2  15736  sylow2alem2  15755  sylow2a  15756  slwhash  15761  sylow2  15763  sylow3lem1  15764  cyggenod  15997  lt6abl  16007  gsumval3  16017  ablfac1c  16132  ablfac1eu  16134  ablfaclem3  16148  fta1blem  20595  vieta1  20733  basellem5  21376  isppw  21406  eupai  22198  derangen2  25699  subfacp1lem3  25707  subfacp1lem5  25709  erdsze2lem1  25728  erdsze2lem2  25729  prodmolem3  26089  prodmolem2a  26090  bpolylem  26924  eldioph2lem1  27749  frlmpwfi  28168  isnumbasgrplem3  28176  idomsubgmo  28420  hash3tr  29093  pr2pwpr  29600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338  ax-cnex 9160  ax-resscn 9161  ax-1cn 9162  ax-icn 9163  ax-addcl 9164  ax-addrcl 9165  ax-mulcl 9166  ax-mulrcl 9167  ax-mulcom 9168  ax-addass 9169  ax-mulass 9170  ax-distr 9171  ax-i2m1 9172  ax-1ne0 9173  ax-1rid 9174  ax-rnegex 9175  ax-rrecex 9176  ax-cnre 9177  ax-pre-lttri 9178  ax-pre-lttrn 9179  ax-pre-ltadd 9180  ax-pre-mulgt0 9181
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-nel 2647  df-ral 2756  df-rex 2757  df-reu 2758  df-rab 2760  df-v 3008  df-sbc 3213  df-csb 3314  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-pss 3369  df-nul 3661  df-if 3813  df-pw 3880  df-sn 3900  df-pr 3901  df-tp 3902  df-op 3903  df-uni 4102  df-int 4139  df-iun 4183  df-br 4303  df-opab 4361  df-mpt 4362  df-tr 4396  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-riota 6026  df-ov 6070  df-oprab 6071  df-mpt2 6072  df-om 6442  df-recs 6745  df-rdg 6780  df-er 7017  df-en 7222  df-dom 7223  df-sdom 7224  df-fin 7225  df-card 7940  df-pnf 9242  df-mnf 9243  df-xr 9244  df-ltxr 9245  df-le 9246  df-sub 9417  df-neg 9418  df-nn 10132  df-n0 10389  df-z 10454  df-uz 10669  df-hash 11896
  Copyright terms: Public domain W3C validator