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

Theorem f1fn 5788
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 5787 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
2 ffn 5737 . 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 5589   -->wf 5590   -1-1->wf1 5591
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 5598  df-f1 5599
This theorem is referenced by:  f1fun  5789  f1rel  5790  f1dm  5791  f1ssr  5793  f1f1orn  5833  f1elima  6170  f1eqcocnv  6203  domunsncan  7629  marypha2  7911  infdifsn  8085  acndom  8444  dfac12lem2  8536  ackbij1  8630  fin23lem32  8736  fin1a2lem5  8796  fin1a2lem6  8797  pwfseqlem1  9048  hashf1lem1  12484  hashf1  12486  odf1o2  16464  kerf1hrm  17261  frlmlbs  18698  f1lindf  18724  2ndcdisj  19823  qtopf1  20183  usgraedgrn  24213  usgfidegfi  24742  erdszelem10  28476  dihfn  36471  dihcl  36473  dih1dimatlem  36532  dochocss  36569
  Copyright terms: Public domain W3C validator