Theorem f1ofn 3685

Description: A one-to-one onto mapping is function on its domain.

Assertion

Ref	Expression
f1ofn	|- (F:A-1-1-onto->B -> F Fn A)

Proof of Theorem f1ofn

Step	Hyp	Ref	Expression
1		f1of 3684	. 2 |- (F:A-1-1-onto->B -> F:A-->B)
2		ffn 3623	. 2 |- (F:A-->B -> F Fn A)
3	1, 2	syl 10	1 |- (F:A-1-1-onto->B -> F Fn A)

Syntax hints:   -> wi 3   Fn wfn 3173  -->wf 3174  -1-1-onto->wf1o 3177

This theorem is referenced by:  f1ofun 3686  fvsnun2 3791  isomin 3894  isoini 3895  isofrlem 3896  breng 4366  f1oeng 4385  phplem4 4500  php3 4504  unfilem3 4535  unifi 4541  fiint 4543  acdc2lem2 7448  acdc5lem2 7451  unbenlem 7464  ruclem6 7475  invfval 8225  shftefif1olem 8696  adjbd1o 9974

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-f 3190  df-f1 3191  df-f1o 3193

Copyright terms: Public domain