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  8123  fnwelem  8133  f1dmvrnfibi  9305  fsuppco  9369  ackbij1b  10237  fin23lem31  10342  fin1a2lem6  10404  hashimarn  14495  hashf1dmrn  14498  ccatf1  14646  gsumval3lem1  20019  gsumval3lem2  20020  usgrfun  29566  trlsegvdeglem6  30647  cycpmrn  33527  cycpmconjslem2  33539  fineqvinfep  35595  elhf  36703