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

Theorem f1f 5581
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 5401 . 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 4819   Fun wfun 5390   -->wf 5392   -1-1->wf1 5393
This theorem is referenced by:  f1fn  5582  f1ss  5586  f1ssres  5588  f1of  5616  dff1o5  5625  fun11iun  5637  f1dmex  5912  cocan1  5965  oacomf1olem  6745  brdomg  7056  f1dom2g  7063  f1domg  7065  dom3d  7087  f1imaen2g  7106  2dom  7117  domdifsn  7129  xpdom2  7141  domunsncan  7146  fodomr  7196  domss2  7204  domssex2  7205  sucdom2  7241  f1finf1o  7273  f1fi  7331  oiexg  7439  hartogslem1  7446  infdifsn  7546  fseqenlem1  7840  fseqenlem2  7841  ac10ct  7850  acndom  7867  acndom2  7870  dfac12lem2  7959  dfac12lem3  7960  ackbij1  8053  fictb  8060  cfsmolem  8085  cfcoflem  8087  cfcof  8089  fin23lem17  8153  fin23lem32  8159  fin23lem39  8165  fin23lem41  8167  fin1a2lem6  8220  fin1a2lem7  8221  iundom2g  8350  alephreg  8392  canthnumlem  8458  canthwelem  8460  pwfseqlem1  8468  pwfseqlem5  8473  seqf1olem1  11291  hashf1rn  11565  hashf1lem1  11633  hashf1lem2  11634  setcmon  14171  odinf  15128  odcl2  15130  odf1o1  15135  sylow1lem2  15162  gsumval3  15443  gsumzcl  15447  gsumzf1o  15448  gsumzaddlem  15455  gsumzmhm  15462  gsumzoppg  15468  dprdf1  15520  2ndcdisj  17442  itg1addlem4  19460  reeff1o  20232  birthdaylem1  20659  basellem3  20734  dchrisum0fno1  21074  ausisusgra  21249  usgrass  21253  uslisumgra  21255  usgra0v  21260  usgraedg2  21264  usgraedgrnv  21266  usgrarnedg  21272  usgraedg4  21274  usgra1v  21277  usgrares1  21292  cusgrarn  21336  fargshiftf1  21474  usgrcyclnl2  21478  qqhre  24184  erdszelem4  24661  erdszelem8  24665  erdszelem9  24666  erdsze2lem2  24671  diophrw  26510  eldioph2lem2  26512  eldioph2  26513  eldioph2b  26514  dnwech  26816  f1lindf  26963  f1linds  26966  lindfmm  26968  seff  27209
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 5401
  Copyright terms: Public domain W3C validator