Theorem f1ofun 4637

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 4636	. 2 |- (F:A-1-1-onto->B -> F Fn A)
2		fnfun 4510	. 2 |- (F Fn A -> Fun F)
3	1, 2	syl 12	1 |- (F:A-1-1-onto->B -> Fun F)

Syntax hints:   -> wi 3  Fun wfun 3992   Fn wfn 3993  -1-1-onto->wf1o 3997

This theorem is referenced by:  f1orel 4638  f1ocnvfv1 4854  f1ocnvfv2 4855  isotr 4874  isotrALT 4875  isofrlem 4878  ac6sfilem3 5508  mapenlem1 5583  php3 5609  uzrdgvali 7714  unbenlem 8773  shftefif1olem 10095  dfrelog 10110  counop 11482  domrancur1c 14550  opncldf2 15403  opncldf3 15404  compfipin0lem 15435  compfipin0 15436  f1ocan1fv 15717  f1ocan2fv 15718  ismtyhmeolem 15950  ismtyres 15954

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 164  df-an 242  df-fn 4009  df-f 4010  df-f1 4011  df-f1o 4013

Copyright terms: Public domain