Theorem f1fun 6745

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

Syntax hints:   → wi 4  Fun wfun 6495   Fn wfn 6496  –1-1→wf1 6498

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 206  df-an 397  df-fn 6504  df-f 6505  df-f1 6506

This theorem is referenced by:  f1cocnv2  6817  f1o2ndf1  8059  fnwelem  8068  f1dmvrnfibi  9287  fsuppco  9347  ackbij1b  10184  fin23lem31  10288  fin1a2lem6  10350  hashimarn  14350  hashf1dmrn  14353  gsumval3lem1  19696  gsumval3lem2  19697  usgrfun  28172  trlsegvdeglem6  29232  ccatf1  31875  cycpmrn  32062  cycpmconjslem2  32074  elhf  34835