Theorem f1fun 6807

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

Syntax hints:   → wi 4  Fun wfun 6557   Fn wfn 6558  –1-1→wf1 6560

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 6566  df-f 6567  df-f1 6568

This theorem is referenced by:  f1cocnv2  6877  f1o2ndf1  8146  fnwelem  8155  f1dmvrnfibi  9379  fsuppco  9440  ackbij1b  10276  fin23lem31  10381  fin1a2lem6  10443  hashimarn  14476  hashf1dmrn  14479  gsumval3lem1  19938  gsumval3lem2  19939  usgrfun  29190  trlsegvdeglem6  30254  ccatf1  32918  cycpmrn  33146  cycpmconjslem2  33158  elhf  36156