Theorem f1ofun 5616

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 5615	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5453	. 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 5346   Fn wfn 5347   -1-1-onto->wf1o 5351

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 5355  df-f 5356  df-f1 5357  df-f1o 5359

This theorem is referenced by:  f1orel  5617  f1oresrab  5842  isose  5994  f1opw  6262  xpcomco  7077  fiintim  7191  f1dmvrnfibi  7211  caseinl  7382  caseinr  7383  ctssdccl  7402  ctssdclemr  7403  fihasheqf1oi  11150  fisumss  12078  ennnfonelemex  13165  ennnfonelemf1  13169  hmeontr  15178