Theorem f1fun 6740

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

Syntax hints:   → wi 4  Fun wfun 6494   Fn wfn 6495  –1-1→wf1 6497

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 6503  df-f 6504  df-f1 6505

This theorem is referenced by:  f1cocnv2  6810  f1o2ndf1  8074  fnwelem  8083  f1dmvrnfibi  9253  fsuppco  9317  ackbij1b  10160  fin23lem31  10265  fin1a2lem6  10327  hashimarn  14375  hashf1dmrn  14378  gsumval3lem1  19846  gsumval3lem2  19847  usgrfun  29243  trlsegvdeglem6  30312  ccatf1  33042  cycpmrn  33237  cycpmconjslem2  33249  fineqvinfep  35303  elhf  36390