Theorem f1ofun 5524

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 5523	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5371	. 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 5265   Fn wfn 5266   -1-1-onto->wf1o 5270

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 5274  df-f 5275  df-f1 5276  df-f1o 5278

This theorem is referenced by:  f1orel  5525  f1oresrab  5745  isose  5890  f1opw  6153  xpcomco  6921  fiintim  7028  f1dmvrnfibi  7046  caseinl  7193  caseinr  7194  ctssdccl  7213  ctssdclemr  7214  fihasheqf1oi  10932  fisumss  11703  ennnfonelemex  12785  ennnfonelemf1  12789  hmeontr  14785