Theorem f1fun 6757

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

Syntax hints:   → wi 4  Fun wfun 6510  –1-1→wf1 6513

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 209  df-an 400  df-fn 6519  df-f 6520  df-f1 6521

This theorem is referenced by:  f1cocnv2  6830  f1o2ndf1  8095  fnwelem  8105  f1dmvrnfibi  9278  fsuppco  9342  ackbij1b  10188  fin23lem31  10294  fin1a2lem6  10356  hashimarn  14447  hashf1dmrn  14450  gsumval3lem1  19936  gsumval3lem2  19937  usgrfun  29316  trlsegvdeglem6  30384  ccatf1  33088  cycpmrn  33284  cycpmconjslem2  33296  fineqvinfep  35382  elhf  36485