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

Theorem f1fn 5619
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 5618 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
2 ffn 5571 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 1  |-  ( F : A -1-1-> B  ->  F  Fn  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Fn wfn 5425   -->wf 5426   -1-1->wf1 5427
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 185  df-an 371  df-f 5434  df-f1 5435
This theorem is referenced by:  f1fun  5620  f1rel  5621  f1dm  5622  f1ssr  5624  f1f1orn  5664  f1elima  5988  f1eqcocnv  6011  domunsncan  7423  marypha2  7701  infdifsn  7874  acndom  8233  dfac12lem2  8325  ackbij1  8419  fin23lem32  8525  fin1a2lem5  8585  fin1a2lem6  8586  pwfseqlem1  8837  hashf1lem1  12220  hashf1  12222  odf1o2  16084  kerf1hrm  16843  frlmlbs  18237  f1lindf  18263  2ndcdisj  19072  qtopf1  19401  usgraedgrn  23312  erdszelem10  27100  usgfidegfi  30539  dihfn  34925  dihcl  34927  dih1dimatlem  34986  dochocss  35023
  Copyright terms: Public domain W3C validator