Theorem f1ofun 5636

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 5635	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5473	. 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 5366   Fn wfn 5367   -1-1-onto->wf1o 5371

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 5375  df-f 5376  df-f1 5377  df-f1o 5379

This theorem is referenced by:  f1orel  5637  f1oresrab  5864  isose  6017  f1opw  6287  xpcomco  7114  fiintim  7228  f1dmvrnfibi  7248  caseinl  7421  caseinr  7422  ctssdccl  7441  ctssdclemr  7442  fihasheqf1oi  11204  fisumss  12137  ballotfilemrv  13241  ennnfonelemex  13283  ennnfonelemf1  13287  hmeontr  15337