Theorem f1ofun 5546

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 5545	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5390	. 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 5284   Fn wfn 5285   -1-1-onto->wf1o 5289

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 5293  df-f 5294  df-f1 5295  df-f1o 5297

This theorem is referenced by:  f1orel  5547  f1oresrab  5768  isose  5913  f1opw  6176  xpcomco  6946  fiintim  7054  f1dmvrnfibi  7072  caseinl  7219  caseinr  7220  ctssdccl  7239  ctssdclemr  7240  fihasheqf1oi  10969  fisumss  11818  ennnfonelemex  12900  ennnfonelemf1  12904  hmeontr  14900