Theorem f1fun 6783

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 6782	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2	1	fnfund 6643	1 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)

This proof depends on syntax axioms:   → wi 4  Fun wfun 6535  –1-1→wf1 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6544  df-f 6545  df-f1 6546

This theorem is used by:  f1cocnv2  6856  f1o2ndf1  8137  fnwelem  8147  f1dmvrnfibi  9335  fsuppco  9399  elhfOLD  9913  ackbij1b  10321  fin23lem31  10426  fin1a2lem6  10488  hashimarn  14590  hashf1dmrn  14593  ccatf1  14741  gsumval3lem1  20126  gsumval3lem2  20127  usgrfun  29746  trlsegvdeglem6  30833  cycpmrn  33752  cycpmconjslem2  33764  fineqvinfep  35851