Theorem f1fun 6716

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

Syntax hints:   → wi 4  Fun wfun 6470   Fn wfn 6471  –1-1→wf1 6473

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 6479  df-f 6480  df-f1 6481

This theorem is referenced by:  f1cocnv2  6786  f1o2ndf1  8047  fnwelem  8056  f1dmvrnfibi  9220  fsuppco  9281  ackbij1b  10124  fin23lem31  10229  fin1a2lem6  10291  hashimarn  14342  hashf1dmrn  14345  gsumval3lem1  19812  gsumval3lem2  19813  usgrfun  29131  trlsegvdeglem6  30197  ccatf1  32922  cycpmrn  33104  cycpmconjslem2  33116  elhf  36208