Theorem f1fun 6672

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

Syntax hints:   → wi 4  Fun wfun 6427   Fn wfn 6428  –1-1→wf1 6430

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 6436  df-f 6437  df-f1 6438

This theorem is referenced by:  f1cocnv2  6744  f1o2ndf1  7963  fnwelem  7972  f1dmvrnfibi  9103  fsuppco  9161  ackbij1b  9995  fin23lem31  10099  fin1a2lem6  10161  hashimarn  14155  gsumval3lem1  19506  gsumval3lem2  19507  usgrfun  27528  trlsegvdeglem6  28589  ccatf1  31223  cycpmrn  31410  cycpmconjslem2  31422  hashf1dmrn  33075  elhf  34476