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  8064  fnwelem  8073  f1dmvrnfibi  9241  fsuppco  9305  ackbij1b  10148  fin23lem31  10253  fin1a2lem6  10315  hashimarn  14363  hashf1dmrn  14366  gsumval3lem1  19834  gsumval3lem2  19835  usgrfun  29231  trlsegvdeglem6  30300  ccatf1  33031  cycpmrn  33225  cycpmconjslem2  33237  fineqvinfep  35281  elhf  36368