Theorem f1fun 6789

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

Syntax hints:   → wi 4  Fun wfun 6537   Fn wfn 6538  –1-1→wf1 6540

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 6546  df-f 6547  df-f1 6548

This theorem is referenced by:  f1cocnv2  6861  f1o2ndf1  8113  fnwelem  8122  f1dmvrnfibi  9342  fsuppco  9403  ackbij1b  10240  fin23lem31  10344  fin1a2lem6  10406  hashimarn  14407  hashf1dmrn  14410  gsumval3lem1  19821  gsumval3lem2  19822  usgrfun  28851  trlsegvdeglem6  29911  ccatf1  32548  cycpmrn  32738  cycpmconjslem2  32750  elhf  35616