Theorem f1ofun 5377

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

Assertion

Ref	Expression
f1ofun	|- ( F : A -1-1-onto-> B -> Fun F )

Proof of Theorem f1ofun

Step	Hyp	Ref	Expression
1		f1ofn 5376	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5228	. 2 |- ( F Fn A -> Fun F )
3	1, 2	syl 14	1 |- ( F : A -1-1-onto-> B -> Fun F )

Syntax hints:   -> wi 4   Fun wfun 5125   Fn wfn 5126   -1-1-onto->wf1o 5130

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

This theorem depends on definitions:  df-bi 116  df-fn 5134  df-f 5135  df-f1 5136  df-f1o 5138

This theorem is referenced by:  f1orel  5378  f1oresrab  5593  isose  5730  f1opw  5985  xpcomco  6728  fiintim  6825  f1dmvrnfibi  6840  caseinl  6984  caseinr  6985  ctssdccl  7004  ctssdclemr  7005  fihasheqf1oi  10566  fisumss  11193  ennnfonelemex  11963  ennnfonelemf1  11967  hmeontr  12521