Theorem f1ofun 5442

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 5441	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5293	. 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 5190   Fn wfn 5191   -1-1-onto->wf1o 5195

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 5199  df-f 5200  df-f1 5201  df-f1o 5203

This theorem is referenced by:  f1orel  5443  f1oresrab  5659  isose  5798  f1opw  6054  xpcomco  6802  fiintim  6904  f1dmvrnfibi  6919  caseinl  7066  caseinr  7067  ctssdccl  7086  ctssdclemr  7087  fihasheqf1oi  10715  fisumss  11348  ennnfonelemex  12362  ennnfonelemf1  12366  hmeontr  13072