Theorem f1fun 6819

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

Syntax hints:   → wi 4  Fun wfun 6567   Fn wfn 6568  –1-1→wf1 6570

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 6576  df-f 6577  df-f1 6578

This theorem is referenced by:  f1cocnv2  6890  f1o2ndf1  8163  fnwelem  8172  f1dmvrnfibi  9409  fsuppco  9471  ackbij1b  10307  fin23lem31  10412  fin1a2lem6  10474  hashimarn  14489  hashf1dmrn  14492  gsumval3lem1  19947  gsumval3lem2  19948  usgrfun  29193  trlsegvdeglem6  30257  ccatf1  32915  cycpmrn  33136  cycpmconjslem2  33148  elhf  36138