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

Theorem f1f 5763
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 5575 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 458 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   `'ccnv 4987   Fun wfun 5564   -->wf 5566   -1-1->wf1 5567
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 369  df-f1 5575
This theorem is referenced by:  f1fn  5764  f1ss  5768  f1ssres  5770  f1of  5798  dff1o5  5807  f1dom3el3dif  6151  cocan1  6169  fun11iun  6733  f1dmex  6743  f1o2ndf1  6881  oacomf1olem  7205  brdomg  7519  f1dom2g  7526  f1domg  7528  dom3d  7550  f1imaen2g  7569  2dom  7581  domdifsn  7593  xpdom2  7605  domunsncan  7610  fodomr  7661  domss2  7669  domssex2  7670  sucdom2  7707  f1finf1o  7739  f1fi  7799  oiexg  7952  hartogslem1  7959  infdifsn  8064  fseqenlem1  8396  fseqenlem2  8397  ac10ct  8406  acndom  8423  acndom2  8426  dfac12lem2  8515  dfac12lem3  8516  ackbij1  8609  fictb  8616  cfsmolem  8641  cfcoflem  8643  cfcof  8645  fin23lem17  8709  fin23lem32  8715  fin23lem39  8721  fin23lem41  8723  fin1a2lem6  8776  fin1a2lem7  8777  iundom2g  8906  alephreg  8948  canthnumlem  9015  canthwelem  9017  pwfseqlem1  9025  pwfseqlem5  9030  seqf1olem1  12131  hashf1rn  12410  hashimarn  12483  hashf1lem1  12491  hashf1lem2  12492  setcmon  15568  odinf  16787  odcl2  16789  odf1o1  16794  sylow1lem2  16821  gsumval3OLD  17110  gsumval3lem1  17111  gsumval3lem2  17112  gsumval3  17113  gsumzcl2  17117  gsumzf1o  17119  gsumzclOLD  17121  gsumzf1oOLD  17122  gsumzaddlem  17136  gsumzaddlemOLD  17138  gsumzmhm  17158  gsumzmhmOLD  17159  gsumzoppg  17168  gsumzoppgOLD  17169  dprdf1  17278  f1lindf  19027  f1linds  19030  lindfmm  19032  mdetunilem8  19291  2ndcdisj  20126  itg1addlem4  22275  reeff1o  23011  birthdaylem1  23482  basellem3  23557  dchrisum0fno1  23897  ushgrauhgra  24508  edgss  24557  ausisusgra  24560  usgrass  24566  uslisumgra  24569  usgra0v  24576  usgraedg2  24580  usgraedgrnv  24582  usgrarnedg  24589  usgraedg4  24592  usgra1v  24595  usgrares1  24615  cusgrarn  24664  fargshiftf1  24842  usgrcyclnl2  24846  clwlkisclwwlklem1  24992  usgravd00  25124  qqhre  28235  esumiun  28326  erdszelem4  28905  erdszelem8  28909  erdszelem9  28910  erdsze2lem2  28915  diophrw  30934  eldioph2lem2  30936  eldioph2  30937  eldioph2b  30938  dnwech  31236  seff  31433  2f1fvneq  32700  usgra2pth  32745  ushguhg  32762
  Copyright terms: Public domain W3C validator