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

Theorem f1f 5786
Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)
Assertion
Ref Expression
f1f

Proof of Theorem f1f
StepHypRef Expression
1 df-f1 5598 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  `'ccnv 5003  Funwfun 5587  -->wf 5589  -1-1->wf1 5590
This theorem is referenced by:  f1fn  5787  f1ss  5791  f1ssres  5793  f1of  5821  dff1o5  5830  f1dom3el3dif  6176  cocan1  6194  fun11iun  6760  f1dmex  6770  f1o2ndf1  6908  oacomf1olem  7232  brdomg  7546  f1dom2g  7553  f1domg  7555  dom3d  7577  f1imaen2g  7596  2dom  7608  domdifsn  7620  xpdom2  7632  domunsncan  7637  fodomr  7688  domss2  7696  domssex2  7697  sucdom2  7734  f1finf1o  7766  f1fi  7827  oiexg  7981  hartogslem1  7988  infdifsn  8094  fseqenlem1  8426  fseqenlem2  8427  ac10ct  8436  acndom  8453  acndom2  8456  dfac12lem2  8545  dfac12lem3  8546  ackbij1  8639  fictb  8646  cfsmolem  8671  cfcoflem  8673  cfcof  8675  fin23lem17  8739  fin23lem32  8745  fin23lem39  8751  fin23lem41  8753  fin1a2lem6  8806  fin1a2lem7  8807  iundom2g  8936  alephreg  8978  canthnumlem  9047  canthwelem  9049  pwfseqlem1  9057  pwfseqlem5  9062  seqf1olem1  12146  hashf1rn  12425  hashimarn  12496  hashf1lem1  12504  hashf1lem2  12505  setcmon  15414  odinf  16585  odcl2  16587  odf1o1  16592  sylow1lem2  16619  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3lem2  16910  gsumval3  16911  gsumzcl2  16915  gsumzf1o  16917  gsumzclOLD  16919  gsumzf1oOLD  16920  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzoppg  16967  gsumzoppgOLD  16968  dprdf1  17080  f1lindf  18857  f1linds  18860  lindfmm  18862  mdetunilem8  19121  2ndcdisj  19957  itg1addlem4  22106  reeff1o  22842  birthdaylem1  23281  basellem3  23356  dchrisum0fno1  23696  ushgrauhgra  24303  edgss  24352  ausisusgra  24355  usgrass  24361  uslisumgra  24364  usgra0v  24371  usgraedg2  24375  usgraedgrnv  24377  usgrarnedg  24384  usgraedg4  24387  usgra1v  24390  usgrares1  24410  cusgrarn  24459  fargshiftf1  24637  usgrcyclnl2  24641  clwlkisclwwlklem1  24787  usgravd00  24919  qqhre  27998  erdszelem4  28638  erdszelem8  28642  erdszelem9  28643  erdsze2lem2  28648  diophrw  30692  eldioph2lem2  30694  eldioph2  30695  eldioph2b  30696  dnwech  30994  seff  31189  2f1fvneq  32307  usgra2pth  32354  ushguhg  32371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-f1 5598
  Copyright terms: Public domain W3C validator