Theorem f1fun 6776

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

Syntax hints:   → wi 4  Fun wfun 6530  –1-1→wf1 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-fn 6539  df-f 6540  df-f1 6541

This theorem is referenced by:  f1cocnv2  6849  f1o2ndf1  8113  fnwelem  8123  f1dmvrnfibi  9294  fsuppco  9358  ackbij1b  10217  fin23lem31  10322  fin1a2lem6  10384  hashimarn  14473  hashf1dmrn  14476  gsumval3lem1  19970  gsumval3lem2  19971  usgrfun  29508  trlsegvdeglem6  30576  ccatf1  33269  cycpmrn  33463  cycpmconjslem2  33475  fineqvinfep  35538  elhf  36666