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

Theorem f1f 5621
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 5438 . 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 4854   Fun wfun 5427   -->wf 5429   -1-1->wf1 5430
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 5438
This theorem is referenced by:  f1fn  5622  f1ss  5626  f1ssres  5628  f1of  5656  dff1o5  5665  f1dom3el3dif  5996  cocan1  6010  fun11iun  6552  f1dmex  6562  f1o2ndf1  6695  oacomf1olem  7018  brdomg  7335  f1dom2g  7342  f1domg  7344  dom3d  7366  f1imaen2g  7385  2dom  7397  domdifsn  7409  xpdom2  7421  domunsncan  7426  fodomr  7477  domss2  7485  domssex2  7486  sucdom2  7522  f1finf1o  7554  f1fi  7613  oiexg  7764  hartogslem1  7771  infdifsn  7877  fseqenlem1  8209  fseqenlem2  8210  ac10ct  8219  acndom  8236  acndom2  8239  dfac12lem2  8328  dfac12lem3  8329  ackbij1  8422  fictb  8429  cfsmolem  8454  cfcoflem  8456  cfcof  8458  fin23lem17  8522  fin23lem32  8528  fin23lem39  8534  fin23lem41  8536  fin1a2lem6  8589  fin1a2lem7  8590  iundom2g  8719  alephreg  8761  canthnumlem  8830  canthwelem  8832  pwfseqlem1  8840  pwfseqlem5  8845  seqf1olem1  11860  hashf1rn  12138  hashimarn  12215  hashf1lem1  12223  hashf1lem2  12224  setcmon  14970  odinf  16079  odcl2  16081  odf1o1  16086  sylow1lem2  16113  gsumval3OLD  16397  gsumval3lem1  16398  gsumval3lem2  16399  gsumval3  16400  gsumzcl2  16404  gsumzf1o  16406  gsumzclOLD  16408  gsumzf1oOLD  16409  gsumzaddlem  16423  gsumzaddlemOLD  16425  gsumzmhm  16445  gsumzmhmOLD  16446  gsumzoppg  16455  gsumzoppgOLD  16456  dprdf1  16545  f1lindf  18266  f1linds  18269  lindfmm  18271  mdetunilem8  18440  2ndcdisj  19075  itg1addlem4  21192  reeff1o  21927  birthdaylem1  22360  basellem3  22435  dchrisum0fno1  22775  ausisusgra  23294  usgrass  23298  uslisumgra  23300  usgra0v  23305  usgraedg2  23309  usgraedgrnv  23311  usgrarnedg  23318  usgraedg4  23320  usgra1v  23323  usgrares1  23338  cusgrarn  23382  fargshiftf1  23538  usgrcyclnl2  23542  qqhre  26461  erdszelem4  27097  erdszelem8  27101  erdszelem9  27102  erdsze2lem2  27107  diophrw  29116  eldioph2lem2  29118  eldioph2  29119  eldioph2b  29120  dnwech  29420  seff  29614  2f1fvneq  30162  usgra2pth  30320  clwlkisclwwlklem1  30468  usgravd00  30557
  Copyright terms: Public domain W3C validator