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

Theorem f1fn 6573
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 6572 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
21ffnd 6512 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6347  1-1wf1 6349
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 208  df-an 397  df-f 6356  df-f1 6357
This theorem is referenced by:  f1fun  6574  f1rel  6575  f1dm  6576  f1ssr  6578  f1f1orn  6623  f1elima  7015  f1eqcocnv  7051  domunsncan  8606  marypha2  8892  infdifsn  9109  acndom  9466  dfac12lem2  9559  ackbij1  9649  fin23lem32  9755  fin1a2lem5  9815  fin1a2lem6  9816  pwfseqlem1  10069  hashf1lem1  13803  hashf1  13805  odf1o2  18618  kerf1ghm  19417  kerf1hrmOLD  19418  frlmlbs  20860  f1lindf  20885  2ndcdisj  21983  qtopf1  22343  clwlkclwwlklem2  27695  f1rnen  30292  erdszelem10  32334  pibt2  34570  dihfn  38274  dihcl  38276  dih1dimatlem  38335  dochocss  38372  isomushgr  43826
  Copyright terms: Public domain W3C validator