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

Theorem f1f 5437
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 5260 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 446 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4688   Fun wfun 5249   -->wf 5251   -1-1->wf1 5252
This theorem is referenced by:  f1fn  5438  f1ss  5442  f1ssres  5444  f1of  5472  dff1o5  5481  fun11iun  5493  f1dmex  5751  cocan1  5801  oacomf1olem  6562  brdomg  6872  f1dom2g  6879  f1domg  6881  dom3d  6903  f1imaen2g  6922  2dom  6933  domdifsn  6945  xpdom2  6957  domunsncan  6962  fodomr  7012  domss2  7020  domssex2  7021  sucdom2  7057  f1finf1o  7086  f1fi  7143  oiexg  7250  hartogslem1  7257  infdifsn  7357  fseqenlem1  7651  fseqenlem2  7652  ac10ct  7661  acndom  7678  acndom2  7681  dfac12lem2  7770  dfac12lem3  7771  ackbij1  7864  fictb  7871  cfsmolem  7896  cfcoflem  7898  cfcof  7900  fin23lem17  7964  fin23lem32  7970  fin23lem39  7976  fin23lem41  7978  fin1a2lem6  8031  fin1a2lem7  8032  iundom2g  8162  alephreg  8204  canthnumlem  8270  canthwelem  8272  pwfseqlem1  8280  pwfseqlem5  8285  seqf1olem1  11085  hashf1lem1  11393  hashf1lem2  11394  setcmon  13919  odinf  14876  odcl2  14878  odf1o1  14883  sylow1lem2  14910  gsumval3  15191  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumzmhm  15210  gsumzoppg  15216  dprdf1  15268  2ndcdisj  17182  itg1addlem4  19054  reeff1o  19823  birthdaylem1  20246  basellem3  20320  dchrisum0fno1  20660  erdszelem4  23136  erdszelem8  23140  erdszelem9  23141  erdsze2lem2  23146  injrec2  24531  injsurinj  24561  diophrw  26250  eldioph2lem2  26252  eldioph2  26253  eldioph2b  26254  dnwech  26557  f1lindf  26704  f1linds  26707  lindfmm  26709  seff  26950  usgrass  27509  uslisumgra  27511  usgra0v  27516  usgraedg2  27520
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 177  df-an 360  df-f1 5260
  Copyright terms: Public domain W3C validator