Theorem fof 5610

Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

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

Proof of Theorem fof

Step	Hyp	Ref	Expression
1		eqimss 3302	. . 3 |- ( ran F = B -> ran F C_ B )
2	1	anim2i 342	. 2 |- ( ( F Fn A /\ ran F = B ) -> ( F Fn A /\ ran F C_ B ) )
3		df-fo 5378	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5376	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5	2, 3, 4	3imtr4i 201	1 |- ( F : A -onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1402   C_ wss 3220   ran crn 4770   Fn wfn 5367   -->wf 5368   -onto->wfo 5370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5376  df-fo 5378

This theorem is referenced by:  fofun  5611  fofn  5612  dffo2  5614  foima  5615  resdif  5656  ffoss  5667  fconstfvm  5924  cocan2  5984  foeqcnvco  5986  focdmex  6334  algrflem  6455  algrflemg  6456  tposf2  6529  mapfoss  6937  mapsn  6962  ssdomg  7055  fopwdom  7126  fidcenumlemrks  7260  fidcenumlemr  7262  ctmlemr  7438  ctm  7439  ctssdclemn0  7440  ctssdccl  7441  ctssdc  7443  enumctlemm  7444  enumct  7445  fodjuomnilemdc  7474  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  suplocexprlemdisj  8077  suplocexprlemub  8080  wrdsymb  11310  ennnfonelemdc  13268  ennnfonelemg  13272  ennnfonelemp1  13275  ennnfonelemhdmp1  13278  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemhom  13284  ctinfomlemom  13296  ctinf  13299  ctiunctlemudc  13306  ctiunctlemf  13307  omctfn  13312  imasival  13604  imasbas  13605  imasplusg  13606  imasmulr  13607  imasaddfnlemg  13612  imasaddvallemg  13613  imasaddflemg  13614  imasmnd2  13736  imasgrp2  13890  mhmid  13895  mhmmnd  13896  mhmfmhm  13897  ghmgrp  13898  ghmfghm  14107  imasring  14342  znunit  14966  znrrg  14967  dvrecap  15737  gausslemma2dlem1f1o  16093  subctctexmid  16944  pw1nct  16947