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

Theorem f1f 5598
Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)
Assertion
Ref Expression
f1f  |-  ( F : A -1-1-> B  ->  F : A --> B )

Proof of Theorem f1f
StepHypRef Expression
1 df-f1 5418 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 447 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4836   Fun wfun 5407   -->wf 5409   -1-1->wf1 5410
This theorem is referenced by:  f1fn  5599  f1ss  5603  f1ssres  5605  f1of  5633  dff1o5  5642  fun11iun  5654  f1dmex  5930  cocan1  5983  f1o2ndf1  6413  oacomf1olem  6766  brdomg  7077  f1dom2g  7084  f1domg  7086  dom3d  7108  f1imaen2g  7127  2dom  7138  domdifsn  7150  xpdom2  7162  domunsncan  7167  fodomr  7217  domss2  7225  domssex2  7226  sucdom2  7262  f1finf1o  7294  f1fi  7352  oiexg  7460  hartogslem1  7467  infdifsn  7567  fseqenlem1  7861  fseqenlem2  7862  ac10ct  7871  acndom  7888  acndom2  7891  dfac12lem2  7980  dfac12lem3  7981  ackbij1  8074  fictb  8081  cfsmolem  8106  cfcoflem  8108  cfcof  8110  fin23lem17  8174  fin23lem32  8180  fin23lem39  8186  fin23lem41  8188  fin1a2lem6  8241  fin1a2lem7  8242  iundom2g  8371  alephreg  8413  canthnumlem  8479  canthwelem  8481  pwfseqlem1  8489  pwfseqlem5  8494  seqf1olem1  11317  hashf1rn  11591  hashf1lem1  11659  hashf1lem2  11660  setcmon  14197  odinf  15154  odcl2  15156  odf1o1  15161  sylow1lem2  15188  gsumval3  15469  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumzmhm  15488  gsumzoppg  15494  dprdf1  15546  2ndcdisj  17472  itg1addlem4  19544  reeff1o  20316  birthdaylem1  20743  basellem3  20818  dchrisum0fno1  21158  ausisusgra  21333  usgrass  21337  uslisumgra  21339  usgra0v  21344  usgraedg2  21348  usgraedgrnv  21350  usgrarnedg  21357  usgraedg4  21359  usgra1v  21362  usgrares1  21377  cusgrarn  21421  fargshiftf1  21577  usgrcyclnl2  21581  qqhre  24339  erdszelem4  24833  erdszelem8  24837  erdszelem9  24838  erdsze2lem2  24843  diophrw  26707  eldioph2lem2  26709  eldioph2  26710  eldioph2b  26711  dnwech  27013  f1lindf  27160  f1linds  27163  lindfmm  27165  seff  27406  2f1fvneq  27958  hashimarn  27994  usgra2pth  28041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-f1 5418
  Copyright terms: Public domain W3C validator