Theorem f1fun 6773

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

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

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 6536  df-f 6537  df-f1 6538

This theorem is used by:  f1cocnv2  6846  f1o2ndf1  8119  fnwelem  8129  f1dmvrnfibi  9308  fsuppco  9372  ackbij1b  10240  fin23lem31  10345  fin1a2lem6  10407  hashimarn  14505  hashf1dmrn  14508  ccatf1  14656  gsumval3lem1  20032  gsumval3lem2  20033  usgrfun  29618  trlsegvdeglem6  30705  cycpmrn  33583  cycpmconjslem2  33595  fineqvinfep  35651  elhf  36754