Theorem f1ofn 3690

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 3689	. 2 |- (F:A-1-1-onto->B -> F:A-->B)
2		ffn 3627	. 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 3177  -->wf 3178  -1-1-onto->wf1o 3181

This theorem is referenced by:  f1ofun 3691  fvsnun2 3796  isomin 3899  isoini 3900  isofrlem 3901  breng 4375  f1oeng 4395  phplem4 4511  php3 4515  php3OLD 4516  unfilem3 4550  unifiOLD 4557  fiint 4559  fiintOLD 4560  acdc2lem2 7489  acdc5lem2 7492  unbenlem 7504  ruclem6 7515  invfval 8261  shftefif1olem 8741  adjbd1o 10018

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

Copyright terms: Public domain