Theorem f1ofun 3688

Description: A one-to-one onto mapping is a function.

Assertion

Ref	Expression
f1ofun	|- (F:A-1-1-onto->B -> Fun F)

Proof of Theorem f1ofun

Step	Hyp	Ref	Expression
1		f1ofn 3687	. 2 |- (F:A-1-1-onto->B -> F Fn A)
2		fnfun 3582	. 2 |- (F Fn A -> Fun F)
3	1, 2	syl 10	1 |- (F:A-1-1-onto->B -> Fun F)

Syntax hints:   -> wi 3  Fun wfun 3173   Fn wfn 3174  -1-1-onto->wf1o 3178

This theorem is referenced by:  f1orel 3689  f1ocnvfv1 3875  f1ocnvfv2 3876  isotr 3894  isotrALT 3895  isofrlem 3898  mapenlem1 4482  php3 4508  uzrdgval 6257  unbenlem 7483  shftefif1olem 8725  dfrelog 8740  counopt 9836

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-fn 3190  df-f 3191  df-f1 3192  df-f1o 3194

Copyright terms: Public domain