Theorem f1ofun 5482

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 5481	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5332	. 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 5229   Fn wfn 5230   -1-1-onto->wf1o 5234

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 5238  df-f 5239  df-f1 5240  df-f1o 5242

This theorem is referenced by:  f1orel  5483  f1oresrab  5702  isose  5843  f1opw  6102  xpcomco  6853  fiintim  6958  f1dmvrnfibi  6974  caseinl  7121  caseinr  7122  ctssdccl  7141  ctssdclemr  7142  fihasheqf1oi  10802  fisumss  11435  ennnfonelemex  12468  ennnfonelemf1  12472  hmeontr  14290