Theorem f1fun 6810

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 6809	. 2 ⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹 Fn 𝐴)
2	1	fnfund 6670	1 ⊢ (𝐹:𝐴⟶1-1𝐵 → Fun 𝐹)

This proof depends on syntax axioms:   → wi 4  Fun wfun 6560  ⟶1-1wf1 6563

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 6569  df-f 6570  df-f1 6571

This theorem is used by:  f1cocnv2  6884  f1o2ndf1  8170  fnwelem  8180  f1dmvrnfibi  9368  fsuppco  9431  elhfOLD  9945  ackbij1b  10355  fin23lem31  10460  fin1a2lem6  10522  hashimarn  14626  hashf1dmrn  14629  ccatf1  14777  gsumval3lem1  20170  gsumval3lem2  20171  usgrfun  29796  trlsegvdeglem6  30883  cycpmrn  33803  cycpmconjslem2  33815  fineqvinfep  35934