Theorem fofun 3664

Description: An onto mapping is a function.

Assertion

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

Proof of Theorem fofun

Step	Hyp	Ref	Expression
1		fof 3663	. 2 |- (F:A-onto->B -> F:A-->B)
2		ffun 3621	. 2 |- (F:A-->B -> Fun F)
3	1, 2	syl 10	1 |- (F:A-onto->B -> Fun F)

Syntax hints:   -> wi 3  Fun wfun 3171  -->wf 3173  -onto->wfo 3175

This theorem is referenced by:  fornex 3670  cbvfo 3876  fodomfi 4546  fodom 4778  brdom3 4781  ruclem10 7470  ruclem11 7471  bcthlem3 7951  grprn 8006  subgres 8069  vafval 8174  smfval 8176  vsfval 8206  domval 10535  codval 10536  idval 10537  cmpval 10538

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049  df-fn 3188  df-f 3189  df-fo 3191

Copyright terms: Public domain