Theorem f1ofun 5621

Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)

Assertion

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

Proof of Theorem f1ofun

Step	Hyp	Ref	Expression
1		f1ofn 5620	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fnfun 5458	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 5351   Fn wfn 5352  –1-1-onto→wf1o 5356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fn 5360  df-f 5361  df-f1 5362  df-f1o 5364

This theorem is referenced by:  f1orel  5622  f1oresrab  5847  isose  6000  f1opw  6270  xpcomco  7090  fiintim  7204  f1dmvrnfibi  7224  caseinl  7395  caseinr  7396  ctssdccl  7415  ctssdclemr  7416  fihasheqf1oi  11175  fisumss  12103  ballotfilemrv  13207  ennnfonelemex  13249  ennnfonelemf1  13253  hmeontr  15290