Theorem f1fun 6729

Description: A one-to-one mapping is a function. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1fun	⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)

Proof of Theorem f1fun

Step	Hyp	Ref	Expression
1		f1fn 6728	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		fnfun 6589	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6483   Fn wfn 6484  –1-1→wf1 6486

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 207  df-an 396  df-fn 6492  df-f 6493  df-f1 6494

This theorem is referenced by:  f1cocnv2  6799  f1o2ndf1  8061  fnwelem  8070  f1dmvrnfibi  9236  fsuppco  9297  ackbij1b  10140  fin23lem31  10245  fin1a2lem6  10307  hashimarn  14354  hashf1dmrn  14357  gsumval3lem1  19825  gsumval3lem2  19826  usgrfun  29157  trlsegvdeglem6  30226  ccatf1  32959  cycpmrn  33153  cycpmconjslem2  33165  elhf  36290