Theorem f1fun 6738

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

Syntax hints:   → wi 4  Fun wfun 6492   Fn wfn 6493  –1-1→wf1 6495

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

This theorem is referenced by:  f1cocnv2  6808  f1o2ndf1  8072  fnwelem  8081  f1dmvrnfibi  9251  fsuppco  9315  ackbij1b  10160  fin23lem31  10265  fin1a2lem6  10327  hashimarn  14402  hashf1dmrn  14405  gsumval3lem1  19880  gsumval3lem2  19881  usgrfun  29227  trlsegvdeglem6  30295  ccatf1  33009  cycpmrn  33204  cycpmconjslem2  33216  fineqvinfep  35269  elhf  36356