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

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

Proof of Theorem f1fn
StepHypRef Expression
1 f1f 6139 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 ffn 6083 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 5921  wf 5922  1-1wf1 5923
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 197  df-an 385  df-f 5930  df-f1 5931
This theorem is referenced by:  f1fun  6141  f1rel  6142  f1dm  6143  f1ssr  6145  f1f1orn  6186  f1elima  6560  f1eqcocnv  6596  domunsncan  8101  marypha2  8386  infdifsn  8592  acndom  8912  dfac12lem2  9004  ackbij1  9098  fin23lem32  9204  fin1a2lem5  9264  fin1a2lem6  9265  pwfseqlem1  9518  hashf1lem1  13277  hashf1  13279  odf1o2  18034  kerf1hrm  18791  frlmlbs  20184  f1lindf  20209  2ndcdisj  21307  qtopf1  21667  clwlkclwwlklem2  26966  erdszelem10  31308  dihfn  36874  dihcl  36876  dih1dimatlem  36935  dochocss  36972
  Copyright terms: Public domain W3C validator