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

Theorem f1fn 6755
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 6754 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
21ffnd 6686 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6510  1-1wf1 6512
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 6519  df-f1 6520
This theorem is referenced by:  f1fun  6756  f1funOLD  6757  f1relOLD  6759  f1dm  6760  f1ssr  6762  f1f1orn  6812  f1elima  7241  f1eqcocnv  7279  domunsncan  9043  f1domfi2  9144  sbthfilem  9160  fodomfir  9266  marypha2  9380  infdifsn  9607  acndom  10002  dfac12lem2  10096  ackbij1  10188  fin23lem32  10296  fin1a2lem5  10356  fin1a2lem6  10357  pwfseqlem1  10611  hashf1lem1  14463  hashf1  14465  kerf1ghm  19268  odf1o2  19594  frlmlbs  21827  f1lindf  21852  2ndcdisj  23494  qtopf1  23854  clwlkclwwlklem2  30146  f1rnen  32778  fineqvinfep  35381  erdszelem10  35503  pibt2  37864  dihfn  41845  dihcl  41847  dih1dimatlem  41906  dochocss  41943  onsucf1o  43802  cantnfub  43851  cantnfub2  43852  gricushgr  48492  grtrimap  48523
  Copyright terms: Public domain W3C validator