Theorem f1fun 6726

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

Syntax hints:   → wi 4  Fun wfun 6480   Fn wfn 6481  –1-1→wf1 6483

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 6489  df-f 6490  df-f1 6491

This theorem is referenced by:  f1cocnv2  6796  f1o2ndf1  8062  fnwelem  8071  f1dmvrnfibi  9250  fsuppco  9311  ackbij1b  10151  fin23lem31  10256  fin1a2lem6  10318  hashimarn  14366  hashf1dmrn  14369  gsumval3lem1  19803  gsumval3lem2  19804  usgrfun  29122  trlsegvdeglem6  30188  ccatf1  32909  cycpmrn  33104  cycpmconjslem2  33116  elhf  36167