Theorem fof 5595

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 3296	. . 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 5363	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5361	. 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 1398   C_ wss 3214   ran crn 4755   Fn wfn 5352   -->wf 5353   -onto->wfo 5355

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227  df-f 5361  df-fo 5363

This theorem is referenced by:  fofun  5596  fofn  5597  dffo2  5599  foima  5600  resdif  5641  ffoss  5652  fconstfvm  5907  cocan2  5967  foeqcnvco  5969  focdmex  6317  algrflem  6438  algrflemg  6439  tposf2  6512  mapsn  6938  ssdomg  7031  fopwdom  7102  fidcenumlemrks  7236  fidcenumlemr  7238  ctmlemr  7412  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  enumct  7419  fodjuomnilemdc  7448  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  suplocexprlemdisj  8051  suplocexprlemub  8054  wrdsymb  11277  ennnfonelemdc  13234  ennnfonelemg  13238  ennnfonelemp1  13241  ennnfonelemhdmp1  13244  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemhom  13250  ctinfomlemom  13262  ctinf  13265  ctiunctlemudc  13272  ctiunctlemf  13273  omctfn  13278  imasival  13570  imasbas  13571  imasplusg  13572  imasmulr  13573  imasaddfnlemg  13578  imasaddvallemg  13579  imasaddflemg  13580  imasmnd2  13707  imasgrp2  13863  mhmid  13868  mhmmnd  13869  mhmfmhm  13870  ghmgrp  13871  ghmfghm  14079  imasring  14307  znunit  14933  znrrg  14934  dvrecap  15704  gausslemma2dlem1f1o  16059  subctctexmid  16900  pw1nct  16903