Theorem f1fun 6656

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

Syntax hints:   → wi 4  Fun wfun 6412   Fn wfn 6413  –1-1→wf1 6415

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 396  df-fn 6421  df-f 6422  df-f1 6423

This theorem is referenced by:  f1cocnv2  6727  f1o2ndf1  7934  fnwelem  7943  f1dmvrnfibi  9033  fsuppco  9091  ackbij1b  9926  fin23lem31  10030  fin1a2lem6  10092  hashimarn  14083  gsumval3lem1  19421  gsumval3lem2  19422  usgrfun  27431  trlsegvdeglem6  28490  ccatf1  31125  cycpmrn  31312  cycpmconjslem2  31324  hashf1dmrn  32975  elhf  34403