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

Theorem f1fn 6740
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 6739 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
21ffnd 6670 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6492  1-1wf1 6494
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 206  df-an 398  df-f 6501  df-f1 6502
This theorem is referenced by:  f1fun  6741  f1rel  6742  f1dm  6743  f1dmOLD  6744  f1ssr  6746  f1f1orn  6796  f1elima  7211  f1eqcocnv  7248  f1eqcocnvOLD  7249  domunsncan  9017  f1domfi2  9130  sbthfilem  9146  marypha2  9376  infdifsn  9594  acndom  9988  dfac12lem2  10081  ackbij1  10175  fin23lem32  10281  fin1a2lem5  10341  fin1a2lem6  10342  pwfseqlem1  10595  hashf1lem1  14354  hashf1lem1OLD  14355  hashf1  14357  odf1o2  19356  kerf1ghm  20178  frlmlbs  21206  f1lindf  21231  2ndcdisj  22810  qtopf1  23170  clwlkclwwlklem2  28947  f1rnen  31546  erdszelem10  33797  pibt2  35891  dihfn  39734  dihcl  39736  dih1dimatlem  39795  dochocss  39832  onsucf1o  41610  cantnfub  41658  cantnfub2  41659  isomushgr  46025
  Copyright terms: Public domain W3C validator