Theorem f1fun 6780

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

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

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 6543  df-f 6544  df-f1 6545

This theorem is used by:  f1cocnv2  6853  f1o2ndf1  8119  fnwelem  8129  f1dmvrnfibi  9300  fsuppco  9364  ackbij1b  10232  fin23lem31  10337  fin1a2lem6  10399  hashimarn  14488  hashf1dmrn  14491  gsumval3lem1  19985  gsumval3lem2  19986  usgrfun  29523  trlsegvdeglem6  30591  ccatf1  33282  cycpmrn  33476  cycpmconjslem2  33488  fineqvinfep  35550  elhf  36678