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

Theorem f1fn 5669
Description: A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.)
Assertion
Ref Expression
f1fn  |-  ( F : A -1-1-> B  ->  F  Fn  A )

Proof of Theorem f1fn
StepHypRef Expression
1 f1f 5668 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
2 ffn 5620 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 1  |-  ( F : A -1-1-> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Fn wfn 5478   -->wf 5479   -1-1->wf1 5480
This theorem is referenced by:  f1fun  5670  f1rel  5671  f1dm  5672  f1ssr  5674  f1f1orn  5714  f1elima  6038  f1eqcocnv  6057  domunsncan  7237  marypha2  7473  infdifsn  7640  acndom  7963  dfac12lem2  8055  ackbij1  8149  fin23lem32  8255  fin1a2lem5  8315  fin1a2lem6  8316  pwfseqlem1  8564  hashf1lem1  11735  hashf1  11737  odf1o2  15238  2ndcdisj  17550  qtopf1  17879  usgraedgrn  21432  kerf1hrm  24293  erdszelem10  24917  frlmlbs  27264  f1lindf  27307  usgfidegfi  28449  dihfn  32164  dihcl  32166  dih1dimatlem  32225  dochocss  32262
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 179  df-an 362  df-f 5487  df-f1 5488
  Copyright terms: Public domain W3C validator