Theorem f1ofun 3691

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 3690	. 2 |- (F:A-1-1-onto->B -> F Fn A)
2		fnfun 3585	. 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 3176   Fn wfn 3177  -1-1-onto->wf1o 3181

This theorem is referenced by:  f1orel 3692  f1ocnvfv1 3878  f1ocnvfv2 3879  isotr 3897  isotrALT 3898  isofrlem 3901  mapenlem1 4489  php3 4515  php3OLD 4516  uzrdgval 6302  unbenlem 7504  shftefif1olem 8741  dfrelog 8756  counopt 9845

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 3193  df-f 3194  df-f1 3195  df-f1o 3197

Copyright terms: Public domain