Theorem f1fun 6740

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

Syntax hints:   → wi 4  Fun wfun 6493   Fn wfn 6494  –1-1→wf1 6496

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 6502  df-f 6503  df-f1 6504

This theorem is referenced by:  f1cocnv2  6810  f1o2ndf1  8078  fnwelem  8087  f1dmvrnfibi  9268  fsuppco  9329  ackbij1b  10167  fin23lem31  10272  fin1a2lem6  10334  hashimarn  14381  hashf1dmrn  14384  gsumval3lem1  19811  gsumval3lem2  19812  usgrfun  29061  trlsegvdeglem6  30127  ccatf1  32843  cycpmrn  33073  cycpmconjslem2  33085  elhf  36135