Theorem f1fun 6551

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

Syntax hints:   → wi 4  Fun wfun 6318   Fn wfn 6319  –1-1→wf1 6321

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 210  df-an 400  df-fn 6327  df-f 6328  df-f1 6329

This theorem is referenced by:  f1cocnv2  6617  f1o2ndf1  7801  fnwelem  7808  f1dmvrnfibi  8792  fsuppco  8849  ackbij1b  9650  fin23lem31  9754  fin1a2lem6  9816  hashimarn  13797  gsumval3lem1  19018  gsumval3lem2  19019  usgrfun  26951  trlsegvdeglem6  28010  ccatf1  30651  cycpmrn  30835  cycpmconjslem2  30847  hashf1dmrn  32465  elhf  33748