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

Theorem f1fn 5787
 Description: A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.)
Assertion
Ref Expression
f1fn

Proof of Theorem f1fn
StepHypRef Expression
1 f1f 5786 . 2
2 ffn 5736 . 2
31, 2syl 16 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590 This theorem is referenced by:  f1fun  5788  f1rel  5789  f1dm  5790  f1ssr  5792  f1f1orn  5832  f1elima  6171  f1eqcocnv  6204  domunsncan  7637  marypha2  7919  infdifsn  8094  acndom  8453  dfac12lem2  8545  ackbij1  8639  fin23lem32  8745  fin1a2lem5  8805  fin1a2lem6  8806  pwfseqlem1  9057  hashf1lem1  12504  hashf1  12506  odf1o2  16593  kerf1hrm  17392  frlmlbs  18831  f1lindf  18857  2ndcdisj  19957  qtopf1  20317  usgraedgrn  24381  usgfidegfi  24910  erdszelem10  28644  dihfn  36995  dihcl  36997  dih1dimatlem  37056  dochocss  37093 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 5597  df-f1 5598
 Copyright terms: Public domain W3C validator