Theorem f1fun 6805

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

Syntax hints:   → wi 4  Fun wfun 6554   Fn wfn 6555  –1-1→wf1 6557

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 6563  df-f 6564  df-f1 6565

This theorem is referenced by:  f1cocnv2  6875  f1o2ndf1  8148  fnwelem  8157  f1dmvrnfibi  9382  fsuppco  9443  ackbij1b  10279  fin23lem31  10384  fin1a2lem6  10446  hashimarn  14480  hashf1dmrn  14483  gsumval3lem1  19924  gsumval3lem2  19925  usgrfun  29176  trlsegvdeglem6  30245  ccatf1  32934  cycpmrn  33164  cycpmconjslem2  33176  elhf  36176