Theorem f1ofun 5444

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 5443	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5295	. 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 5192   Fn wfn 5193   -1-1-onto->wf1o 5197

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 5201  df-f 5202  df-f1 5203  df-f1o 5205

This theorem is referenced by:  f1orel  5445  f1oresrab  5661  isose  5800  f1opw  6056  xpcomco  6804  fiintim  6906  f1dmvrnfibi  6921  caseinl  7068  caseinr  7069  ctssdccl  7088  ctssdclemr  7089  fihasheqf1oi  10722  fisumss  11355  ennnfonelemex  12369  ennnfonelemf1  12373  hmeontr  13107