Theorem f1ofun 5502

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 5501	. 2 |- ( F : A -1-1-onto-> B -> F Fn A )
2		fnfun 5351	. 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 5248   Fn wfn 5249   -1-1-onto->wf1o 5253

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 5257  df-f 5258  df-f1 5259  df-f1o 5261

This theorem is referenced by:  f1orel  5503  f1oresrab  5723  isose  5864  f1opw  6125  xpcomco  6880  fiintim  6985  f1dmvrnfibi  7003  caseinl  7150  caseinr  7151  ctssdccl  7170  ctssdclemr  7171  fihasheqf1oi  10858  fisumss  11535  ennnfonelemex  12571  ennnfonelemf1  12575  hmeontr  14481