Theorem f1fun 6774

Description: A one-to-one mapping is a function. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
f1fun	⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)

Proof of Theorem f1fun

Step	Hyp	Ref	Expression
1		f1fn 6773	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2	1	fnfund 6634	1 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6528  –1-1→wf1 6531

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 401  df-fn 6537  df-f 6538  df-f1 6539

This theorem is referenced by:  f1cocnv2  6847  f1o2ndf1  8113  fnwelem  8123  f1dmvrnfibi  9294  fsuppco  9358  ackbij1b  10217  fin23lem31  10323  fin1a2lem6  10385  hashimarn  14473  hashf1dmrn  14476  gsumval3lem1  19971  gsumval3lem2  19972  usgrfun  29445  trlsegvdeglem6  30513  ccatf1  33206  cycpmrn  33400  cycpmconjslem2  33412  fineqvinfep  35457  elhf  36561