Theorem f1ofun 5369

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 5368	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5220	. 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 5117   Fn wfn 5118   -1-1-onto->wf1o 5122

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 5126  df-f 5127  df-f1 5128  df-f1o 5130

This theorem is referenced by:  f1orel  5370  f1oresrab  5585  isose  5722  f1opw  5977  xpcomco  6720  fiintim  6817  f1dmvrnfibi  6832  caseinl  6976  caseinr  6977  ctssdccl  6996  ctssdclemr  6997  fihasheqf1oi  10534  fisumss  11161  ennnfonelemex  11927  ennnfonelemf1  11931  hmeontr  12482