Theorem f1fun 6758

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

Syntax hints:   → wi 4  Fun wfun 6505   Fn wfn 6506  –1-1→wf1 6508

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 6514  df-f 6515  df-f1 6516

This theorem is referenced by:  f1cocnv2  6828  f1o2ndf1  8101  fnwelem  8110  f1dmvrnfibi  9292  fsuppco  9353  ackbij1b  10191  fin23lem31  10296  fin1a2lem6  10358  hashimarn  14405  hashf1dmrn  14408  gsumval3lem1  19835  gsumval3lem2  19836  usgrfun  29085  trlsegvdeglem6  30154  ccatf1  32870  cycpmrn  33100  cycpmconjslem2  33112  elhf  36162