Theorem fof 5477

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 3234	. . 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 5261	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5259	. 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 1364   C_ wss 3154   ran crn 4661   Fn wfn 5250   -->wf 5251   -onto->wfo 5253

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167  df-f 5259  df-fo 5261

This theorem is referenced by:  fofun  5478  fofn  5479  dffo2  5481  foima  5482  resdif  5523  ffoss  5533  fconstfvm  5777  cocan2  5832  foeqcnvco  5834  focdmex  6169  algrflem  6284  algrflemg  6285  tposf2  6323  mapsn  6746  ssdomg  6834  fopwdom  6894  fidcenumlemrks  7014  fidcenumlemr  7016  ctmlemr  7169  ctm  7170  ctssdclemn0  7171  ctssdccl  7172  ctssdc  7174  enumctlemm  7175  enumct  7176  fodjuomnilemdc  7205  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  suplocexprlemdisj  7782  suplocexprlemub  7785  wrdsymb  10944  ennnfonelemdc  12559  ennnfonelemg  12563  ennnfonelemp1  12566  ennnfonelemhdmp1  12569  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemhom  12575  ctinfomlemom  12587  ctinf  12590  ctiunctlemudc  12597  ctiunctlemf  12598  omctfn  12603  imasival  12892  imasbas  12893  imasplusg  12894  imasmulr  12895  imasaddfnlemg  12900  imasaddvallemg  12901  imasaddflemg  12902  imasgrp2  13183  mhmid  13188  mhmmnd  13189  mhmfmhm  13190  ghmgrp  13191  ghmfghm  13399  imasring  13563  znunit  14158  znrrg  14159  dvrecap  14892  gausslemma2dlem1f1o  15217  subctctexmid  15561  pw1nct  15563