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

Theorem f1fn 5603
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 5602 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
2 ffn 5554 . 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 5412   -->wf 5413   -1-1->wf1 5414
This theorem is referenced by:  f1fun  5604  f1rel  5605  f1dm  5606  f1ssr  5608  f1f1orn  5648  f1elima  5972  f1eqcocnv  5991  domunsncan  7171  marypha2  7406  infdifsn  7571  acndom  7892  dfac12lem2  7984  ackbij1  8078  fin23lem32  8184  fin1a2lem5  8244  fin1a2lem6  8245  pwfseqlem1  8493  hashf1lem1  11663  hashf1  11665  odf1o2  15166  2ndcdisj  17476  qtopf1  17805  usgraedgrn  21358  kerf1hrm  24219  erdszelem10  24843  frlmlbs  27121  f1lindf  27164  usgfidegfi  28094  dihfn  31755  dihcl  31757  dih1dimatlem  31816  dochocss  31853
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-f 5421  df-f1 5422
  Copyright terms: Public domain W3C validator