Theorem fof 5483

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 3238	. . 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 5265	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5263	. 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 3157   ran crn 4665   Fn wfn 5254   -->wf 5255   -onto->wfo 5257

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-f 5263  df-fo 5265

This theorem is referenced by:  fofun  5484  fofn  5485  dffo2  5487  foima  5488  resdif  5529  ffoss  5539  fconstfvm  5783  cocan2  5838  foeqcnvco  5840  focdmex  6181  algrflem  6296  algrflemg  6297  tposf2  6335  mapsn  6758  ssdomg  6846  fopwdom  6906  fidcenumlemrks  7028  fidcenumlemr  7030  ctmlemr  7183  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  enumct  7190  fodjuomnilemdc  7219  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  suplocexprlemdisj  7804  suplocexprlemub  7807  wrdsymb  10979  ennnfonelemdc  12641  ennnfonelemg  12645  ennnfonelemp1  12648  ennnfonelemhdmp1  12651  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemhom  12657  ctinfomlemom  12669  ctinf  12672  ctiunctlemudc  12679  ctiunctlemf  12680  omctfn  12685  imasival  13008  imasbas  13009  imasplusg  13010  imasmulr  13011  imasaddfnlemg  13016  imasaddvallemg  13017  imasaddflemg  13018  imasmnd2  13154  imasgrp2  13316  mhmid  13321  mhmmnd  13322  mhmfmhm  13323  ghmgrp  13324  ghmfghm  13532  imasring  13696  znunit  14291  znrrg  14292  dvrecap  15033  gausslemma2dlem1f1o  15385  subctctexmid  15731  pw1nct  15734