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

Theorem f1fn 6000
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 5999 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 ffn 5944 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 5785  wf 5786  1-1wf1 5787
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 196  df-an 385  df-f 5794  df-f1 5795
This theorem is referenced by:  f1fun  6001  f1rel  6002  f1dm  6003  f1ssr  6005  f1f1orn  6046  f1elima  6399  f1eqcocnv  6434  domunsncan  7923  marypha2  8206  infdifsn  8415  acndom  8735  dfac12lem2  8827  ackbij1  8921  fin23lem32  9027  fin1a2lem5  9087  fin1a2lem6  9088  pwfseqlem1  9337  hashf1lem1  13051  hashf1  13053  odf1o2  17760  kerf1hrm  18515  frlmlbs  19903  f1lindf  19928  2ndcdisj  21017  qtopf1  21377  usgraedgrn  25704  usgfidegfi  26231  erdszelem10  30230  dihfn  35369  dihcl  35371  dih1dimatlem  35430  dochocss  35467  clwlkclwwlklem2  41201
  Copyright terms: Public domain W3C validator