Theorem f1ofun 5573

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 5572	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5417	. 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 5311   Fn wfn 5312   -1-1-onto->wf1o 5316

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 5320  df-f 5321  df-f1 5322  df-f1o 5324

This theorem is referenced by:  f1orel  5574  f1oresrab  5799  isose  5944  f1opw  6211  xpcomco  6981  fiintim  7089  f1dmvrnfibi  7107  caseinl  7254  caseinr  7255  ctssdccl  7274  ctssdclemr  7275  fihasheqf1oi  11004  fisumss  11898  ennnfonelemex  12980  ennnfonelemf1  12984  hmeontr  14981