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

Theorem f1fn 6317
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 6316 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
21ffnd 6257 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6096  1-1wf1 6098
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 199  df-an 386  df-f 6105  df-f1 6106
This theorem is referenced by:  f1fun  6318  f1rel  6319  f1dm  6320  f1ssr  6322  f1f1orn  6367  f1elima  6748  f1eqcocnv  6784  domunsncan  8302  marypha2  8587  infdifsn  8804  acndom  9160  dfac12lem2  9254  ackbij1  9348  fin23lem32  9454  fin1a2lem5  9514  fin1a2lem6  9515  pwfseqlem1  9768  hashf1lem1  13488  hashf1  13490  odf1o2  18301  kerf1hrm  19061  frlmlbs  20461  f1lindf  20486  2ndcdisj  21588  qtopf1  21948  clwlkclwwlklem2  27293  erdszelem10  31699  dihfn  37289  dihcl  37291  dih1dimatlem  37350  dochocss  37387  isomushgr  42496
  Copyright terms: Public domain W3C validator