Theorem f1fun 6732

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 6731	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		fnfun 6592	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6486   Fn wfn 6487  –1-1→wf1 6489

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-fn 6495  df-f 6496  df-f1 6497

This theorem is referenced by:  f1cocnv2  6802  f1o2ndf1  8065  fnwelem  8074  f1dmvrnfibi  9244  fsuppco  9308  ackbij1b  10151  fin23lem31  10256  fin1a2lem6  10318  hashimarn  14393  hashf1dmrn  14396  gsumval3lem1  19871  gsumval3lem2  19872  usgrfun  29241  trlsegvdeglem6  30310  ccatf1  33024  cycpmrn  33219  cycpmconjslem2  33231  fineqvinfep  35285  elhf  36372