Theorem f1fun 6778

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

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

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 6540  df-f 6541  df-f1 6542

This theorem is used by:  f1cocnv2  6851  f1o2ndf1  8131  fnwelem  8141  f1dmvrnfibi  9323  fsuppco  9387  elhfOLD  9901  ackbij1b  10309  fin23lem31  10414  fin1a2lem6  10476  hashimarn  14578  hashf1dmrn  14581  ccatf1  14729  gsumval3lem1  20112  gsumval3lem2  20113  usgrfun  29732  trlsegvdeglem6  30819  cycpmrn  33697  cycpmconjslem2  33709  fineqvinfep  35776