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

Theorem f1fn 5544
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 5543 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
2 ffn 5495 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 15 1  |-  ( F : A -1-1-> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Fn wfn 5353   -->wf 5354   -1-1->wf1 5355
This theorem is referenced by:  f1fun  5545  f1rel  5546  f1dm  5547  f1ssr  5549  f1f1orn  5589  f1elima  5909  f1eqcocnv  5928  domunsncan  7105  marypha2  7339  infdifsn  7504  acndom  7825  dfac12lem2  7917  ackbij1  8011  fin23lem32  8117  fin1a2lem5  8177  fin1a2lem6  8178  pwfseqlem1  8427  hashf1lem1  11591  hashf1  11593  odf1o2  15094  2ndcdisj  17399  qtopf1  17724  usgraedgrn  21078  kerf1hrm  23627  erdszelem10  24334  frlmlbs  26755  f1lindf  26798  dihfn  31529  dihcl  31531  dih1dimatlem  31590  dochocss  31627
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-f 5362  df-f1 5363
  Copyright terms: Public domain W3C validator