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

Theorem f1f 5631
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 5451 . 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 4869   Fun wfun 5440   -->wf 5442   -1-1->wf1 5443
This theorem is referenced by:  f1fn  5632  f1ss  5636  f1ssres  5638  f1of  5666  dff1o5  5675  fun11iun  5687  f1dmex  5963  cocan1  6016  f1o2ndf1  6446  oacomf1olem  6799  brdomg  7110  f1dom2g  7117  f1domg  7119  dom3d  7141  f1imaen2g  7160  2dom  7171  domdifsn  7183  xpdom2  7195  domunsncan  7200  fodomr  7250  domss2  7258  domssex2  7259  sucdom2  7295  f1finf1o  7327  f1fi  7385  oiexg  7496  hartogslem1  7503  infdifsn  7603  fseqenlem1  7897  fseqenlem2  7898  ac10ct  7907  acndom  7924  acndom2  7927  dfac12lem2  8016  dfac12lem3  8017  ackbij1  8110  fictb  8117  cfsmolem  8142  cfcoflem  8144  cfcof  8146  fin23lem17  8210  fin23lem32  8216  fin23lem39  8222  fin23lem41  8224  fin1a2lem6  8277  fin1a2lem7  8278  iundom2g  8407  alephreg  8449  canthnumlem  8515  canthwelem  8517  pwfseqlem1  8525  pwfseqlem5  8530  seqf1olem1  11354  hashf1rn  11628  hashf1lem1  11696  hashf1lem2  11697  setcmon  14234  odinf  15191  odcl2  15193  odf1o1  15198  sylow1lem2  15225  gsumval3  15506  gsumzcl  15510  gsumzf1o  15511  gsumzaddlem  15518  gsumzmhm  15525  gsumzoppg  15531  dprdf1  15583  2ndcdisj  17511  itg1addlem4  19583  reeff1o  20355  birthdaylem1  20782  basellem3  20857  dchrisum0fno1  21197  ausisusgra  21372  usgrass  21376  uslisumgra  21378  usgra0v  21383  usgraedg2  21387  usgraedgrnv  21389  usgrarnedg  21396  usgraedg4  21398  usgra1v  21401  usgrares1  21416  cusgrarn  21460  fargshiftf1  21616  usgrcyclnl2  21620  qqhre  24378  erdszelem4  24872  erdszelem8  24876  erdszelem9  24877  erdsze2lem2  24882  diophrw  26798  eldioph2lem2  26800  eldioph2  26801  eldioph2b  26802  dnwech  27104  f1lindf  27250  f1linds  27253  lindfmm  27255  seff  27496  2f1fvneq  28053  hashimarn  28131  usgra2pth  28254
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 5451
  Copyright terms: Public domain W3C validator