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

Theorem f1fn 6805
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 6804 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
21ffnd 6737 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6556  1-1wf1 6558
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 207  df-an 396  df-f 6565  df-f1 6566
This theorem is referenced by:  f1fun  6806  f1rel  6807  f1dm  6808  f1ssr  6810  f1f1orn  6859  f1elima  7283  f1eqcocnv  7321  domunsncan  9112  f1domfi2  9222  sbthfilem  9238  fodomfir  9368  marypha2  9479  infdifsn  9697  acndom  10091  dfac12lem2  10185  ackbij1  10277  fin23lem32  10384  fin1a2lem5  10444  fin1a2lem6  10445  pwfseqlem1  10698  hashf1lem1  14494  hashf1  14496  kerf1ghm  19265  odf1o2  19591  frlmlbs  21817  f1lindf  21842  2ndcdisj  23464  qtopf1  23824  clwlkclwwlklem2  30019  f1rnen  32639  erdszelem10  35205  pibt2  37418  dihfn  41270  dihcl  41272  dih1dimatlem  41331  dochocss  41368  onsucf1o  43285  cantnfub  43334  cantnfub2  43335  gricushgr  47886  grtrimap  47915
  Copyright terms: Public domain W3C validator