Theorem f1fun 6571

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

Syntax hints:   → wi 4  Fun wfun 6343   Fn wfn 6344  –1-1→wf1 6346

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 209  df-an 399  df-fn 6352  df-f 6353  df-f1 6354

This theorem is referenced by:  f1cocnv2  6636  f1o2ndf1  7812  fnwelem  7819  f1dmvrnfibi  8802  fsuppco  8859  ackbij1b  9655  fin23lem31  9759  fin1a2lem6  9821  hashimarn  13795  gsumval3lem1  19019  gsumval3lem2  19020  usgrfun  26937  trlsegvdeglem6  27998  ccatf1  30620  cycpmrn  30780  cycpmconjslem2  30792  hashf1dmrn  32350  elhf  33630