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

Theorem f1f 5779
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 5591 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 460 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   `'ccnv 4998   Fun wfun 5580   -->wf 5582   -1-1->wf1 5583
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 5591
This theorem is referenced by:  f1fn  5780  f1ss  5784  f1ssres  5786  f1of  5814  dff1o5  5823  f1dom3el3dif  6162  cocan1  6180  fun11iun  6741  f1dmex  6751  f1o2ndf1  6888  oacomf1olem  7210  brdomg  7523  f1dom2g  7530  f1domg  7532  dom3d  7554  f1imaen2g  7573  2dom  7585  domdifsn  7597  xpdom2  7609  domunsncan  7614  fodomr  7665  domss2  7673  domssex2  7674  sucdom2  7711  f1finf1o  7743  f1fi  7803  oiexg  7956  hartogslem1  7963  infdifsn  8069  fseqenlem1  8401  fseqenlem2  8402  ac10ct  8411  acndom  8428  acndom2  8431  dfac12lem2  8520  dfac12lem3  8521  ackbij1  8614  fictb  8621  cfsmolem  8646  cfcoflem  8648  cfcof  8650  fin23lem17  8714  fin23lem32  8720  fin23lem39  8726  fin23lem41  8728  fin1a2lem6  8781  fin1a2lem7  8782  iundom2g  8911  alephreg  8953  canthnumlem  9022  canthwelem  9024  pwfseqlem1  9032  pwfseqlem5  9037  seqf1olem1  12110  hashf1rn  12389  hashimarn  12458  hashf1lem1  12466  hashf1lem2  12467  setcmon  15268  odinf  16381  odcl2  16383  odf1o1  16388  sylow1lem2  16415  gsumval3OLD  16699  gsumval3lem1  16700  gsumval3lem2  16701  gsumval3  16702  gsumzcl2  16706  gsumzf1o  16708  gsumzclOLD  16710  gsumzf1oOLD  16711  gsumzaddlem  16725  gsumzaddlemOLD  16727  gsumzmhm  16748  gsumzmhmOLD  16749  gsumzoppg  16758  gsumzoppgOLD  16759  dprdf1  16870  f1lindf  18624  f1linds  18627  lindfmm  18629  mdetunilem8  18888  2ndcdisj  19723  itg1addlem4  21841  reeff1o  22576  birthdaylem1  23009  basellem3  23084  dchrisum0fno1  23424  ushgrauhgra  23979  edgss  24028  ausisusgra  24031  usgrass  24037  uslisumgra  24040  usgra0v  24047  usgraedg2  24051  usgraedgrnv  24053  usgrarnedg  24060  usgraedg4  24063  usgra1v  24066  usgrares1  24086  cusgrarn  24135  fargshiftf1  24313  usgrcyclnl2  24317  clwlkisclwwlklem1  24463  usgravd00  24595  qqhre  27634  erdszelem4  28278  erdszelem8  28282  erdszelem9  28283  erdsze2lem2  28288  diophrw  30296  eldioph2lem2  30298  eldioph2  30299  eldioph2b  30300  dnwech  30598  seff  30792  2f1fvneq  31776  usgra2pth  31823  ushguhg  31840
  Copyright terms: Public domain W3C validator