Theorem f1fun 6781

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

Syntax hints:   → wi 4  Fun wfun 6530   Fn wfn 6531  –1-1→wf1 6533

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 6539  df-f 6540  df-f1 6541

This theorem is referenced by:  f1cocnv2  6851  f1o2ndf1  8126  fnwelem  8135  f1dmvrnfibi  9358  fsuppco  9419  ackbij1b  10257  fin23lem31  10362  fin1a2lem6  10424  hashimarn  14463  hashf1dmrn  14466  gsumval3lem1  19891  gsumval3lem2  19892  usgrfun  29142  trlsegvdeglem6  30211  ccatf1  32929  cycpmrn  33159  cycpmconjslem2  33171  elhf  36197