Theorem f1ofun 5523

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 5522	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5370	. 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 5264   Fn wfn 5265   -1-1-onto->wf1o 5269

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 5273  df-f 5274  df-f1 5275  df-f1o 5277

This theorem is referenced by:  f1orel  5524  f1oresrab  5744  isose  5889  f1opw  6152  xpcomco  6920  fiintim  7027  f1dmvrnfibi  7045  caseinl  7192  caseinr  7193  ctssdccl  7212  ctssdclemr  7213  fihasheqf1oi  10930  fisumss  11645  ennnfonelemex  12727  ennnfonelemf1  12731  hmeontr  14727