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

Theorem f1fn 5438
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 5437 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
2 ffn 5389 . 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 5250   -->wf 5251   -1-1->wf1 5252
This theorem is referenced by:  f1fun  5439  f1rel  5440  f1dm  5441  f1ssr  5443  f1f1orn  5483  f1elima  5787  f1eqcocnv  5805  domunsncan  6962  marypha2  7192  infdifsn  7357  acndom  7678  dfac12lem2  7770  ackbij1  7864  fin23lem32  7970  fin1a2lem5  8030  fin1a2lem6  8031  pwfseqlem1  8280  hashf1lem1  11393  hashf1  11395  odf1o2  14884  2ndcdisj  17182  qtopf1  17507  erdszelem10  23731  frlmlbs  27249  f1lindf  27292  usgraedgrn  28125  dihfn  31458  dihcl  31460  dih1dimatlem  31519  dochocss  31556
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 5259  df-f1 5260
  Copyright terms: Public domain W3C validator