Theorem f1fun 6725

Description: A one-to-one mapping is a function. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1fun	⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)

Proof of Theorem f1fun

Step	Hyp	Ref	Expression
1		f1fn 6724	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		fnfun 6585	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6479   Fn wfn 6480  –1-1→wf1 6482

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 208  df-an 397  df-fn 6488  df-f 6489  df-f1 6490

This theorem is referenced by:  f1cocnv2  6795  f1o2ndf1  8061  fnwelem  8071  f1dmvrnfibi  9241  fsuppco  9305  ackbij1b  10151  fin23lem31  10256  fin1a2lem6  10318  hashimarn  14393  hashf1dmrn  14396  gsumval3lem1  19871  gsumval3lem2  19872  usgrfun  29245  trlsegvdeglem6  30313  ccatf1  33028  cycpmrn  33224  cycpmconjslem2  33236  fineqvinfep  35306  elhf  36402