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

Theorem f1fn 6761
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 6760 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
21ffnd 6692 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6516  1-1wf1 6518
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 209  df-an 400  df-f 6525  df-f1 6526
This theorem is referenced by:  f1fun  6762  f1funOLD  6763  f1relOLD  6765  f1dm  6766  f1ssr  6768  f1f1orn  6818  f1elima  7247  f1eqcocnv  7285  domunsncan  9049  f1domfi2  9150  sbthfilem  9166  fodomfir  9272  marypha2  9385  infdifsn  9612  acndom  10007  dfac12lem2  10101  ackbij1  10193  fin23lem32  10301  fin1a2lem5  10361  fin1a2lem6  10362  pwfseqlem1  10616  hashf1lem1  14468  hashf1  14470  kerf1ghm  19287  odf1o2  19613  frlmlbs  21846  f1lindf  21871  2ndcdisj  23513  qtopf1  23873  clwlkclwwlklem2  30199  f1rnen  32827  fineqvinfep  35418  vonf1wev  35448  erdszelem10  35547  pibt2  37908  dihfn  41889  dihcl  41891  dih1dimatlem  41950  dochocss  41987  onsucf1o  43846  cantnfub  43895  cantnfub2  43896  gricushgr  48536  grtrimap  48567
  Copyright terms: Public domain W3C validator