Theorem f1fun 6790

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

Syntax hints:   → wi 4  Fun wfun 6538   Fn wfn 6539  –1-1→wf1 6541

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 206  df-an 398  df-fn 6547  df-f 6548  df-f1 6549

This theorem is referenced by:  f1cocnv2  6862  f1o2ndf1  8108  fnwelem  8117  f1dmvrnfibi  9336  fsuppco  9397  ackbij1b  10234  fin23lem31  10338  fin1a2lem6  10400  hashimarn  14400  hashf1dmrn  14403  gsumval3lem1  19773  gsumval3lem2  19774  usgrfun  28418  trlsegvdeglem6  29478  ccatf1  32115  cycpmrn  32302  cycpmconjslem2  32314  elhf  35146