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

Theorem f1f 5603
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 5420 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 457 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   `'ccnv 4835   Fun wfun 5409   -->wf 5411   -1-1->wf1 5412
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 5420
This theorem is referenced by:  f1fn  5604  f1ss  5608  f1ssres  5610  f1of  5638  dff1o5  5647  f1dom3el3dif  5978  cocan1  5992  fun11iun  6536  f1dmex  6546  f1o2ndf1  6679  oacomf1olem  6999  brdomg  7316  f1dom2g  7323  f1domg  7325  dom3d  7347  f1imaen2g  7366  2dom  7378  domdifsn  7390  xpdom2  7402  domunsncan  7407  fodomr  7458  domss2  7466  domssex2  7467  sucdom2  7503  f1finf1o  7535  f1fi  7594  oiexg  7745  hartogslem1  7752  infdifsn  7858  fseqenlem1  8190  fseqenlem2  8191  ac10ct  8200  acndom  8217  acndom2  8220  dfac12lem2  8309  dfac12lem3  8310  ackbij1  8403  fictb  8410  cfsmolem  8435  cfcoflem  8437  cfcof  8439  fin23lem17  8503  fin23lem32  8509  fin23lem39  8515  fin23lem41  8517  fin1a2lem6  8570  fin1a2lem7  8571  iundom2g  8700  alephreg  8742  canthnumlem  8811  canthwelem  8813  pwfseqlem1  8821  pwfseqlem5  8826  seqf1olem1  11841  hashf1rn  12119  hashimarn  12196  hashf1lem1  12204  hashf1lem2  12205  setcmon  14951  odinf  16057  odcl2  16059  odf1o1  16064  sylow1lem2  16091  gsumval3OLD  16375  gsumval3lem1  16376  gsumval3lem2  16377  gsumval3  16378  gsumzcl2  16382  gsumzf1o  16384  gsumzclOLD  16386  gsumzf1oOLD  16387  gsumzaddlem  16401  gsumzaddlemOLD  16403  gsumzmhm  16422  gsumzmhmOLD  16423  gsumzoppg  16432  gsumzoppgOLD  16433  dprdf1  16520  f1lindf  18210  f1linds  18213  lindfmm  18215  mdetunilem8  18384  2ndcdisj  19019  itg1addlem4  21136  reeff1o  21871  birthdaylem1  22304  basellem3  22379  dchrisum0fno1  22719  ausisusgra  23214  usgrass  23218  uslisumgra  23220  usgra0v  23225  usgraedg2  23229  usgraedgrnv  23231  usgrarnedg  23238  usgraedg4  23240  usgra1v  23243  usgrares1  23258  cusgrarn  23302  fargshiftf1  23458  usgrcyclnl2  23462  qqhre  26382  erdszelem4  27012  erdszelem8  27016  erdszelem9  27017  erdsze2lem2  27022  diophrw  29022  eldioph2lem2  29024  eldioph2  29025  eldioph2b  29026  dnwech  29326  seff  29520  2f1fvneq  30068  usgra2pth  30226  clwlkisclwwlklem1  30374  usgravd00  30463
  Copyright terms: Public domain W3C validator