Theorem f1ofun 5464

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 5463	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5314	. 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 5211   Fn wfn 5212   -1-1-onto->wf1o 5216

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 5220  df-f 5221  df-f1 5222  df-f1o 5224

This theorem is referenced by:  f1orel  5465  f1oresrab  5682  isose  5822  f1opw  6078  xpcomco  6826  fiintim  6928  f1dmvrnfibi  6943  caseinl  7090  caseinr  7091  ctssdccl  7110  ctssdclemr  7111  fihasheqf1oi  10767  fisumss  11400  ennnfonelemex  12415  ennnfonelemf1  12419  hmeontr  13816