Theorem fof 5795

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 3556	. . 3 |- ( ran F = B -> ran F C_ B )
2	1	anim2i 569	. 2 |- ( ( F Fn A /\ ran F = B ) -> ( F Fn A /\ ran F C_ B ) )
3		df-fo 5594	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5592	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5	2, 3, 4	3imtr4i 266	1 |- ( F : A -onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   C_ wss 3476   ran crn 5000   Fn wfn 5583   -->wf 5584   -onto->wfo 5586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-f 5592  df-fo 5594

This theorem is referenced by:  fofun  5796  fofn  5797  dffo2  5799  foima  5800  resdif  5836  fconst5  6118  fconstfv  6123  cocan2  6183  foeqcnvco  6191  soisoi  6212  ffoss  6745  fornex  6753  algrflem  6892  tposf2  6979  smoiso2  7040  mapsn  7460  ssdomg  7561  fopwdom  7625  unfilem2  7785  fodomfib  7800  fofinf1o  7801  brwdomn0  7995  fowdom  7997  wdomtr  8001  wdomima2g  8012  fodomfi2  8441  wdomfil  8442  alephiso  8479  iunfictbso  8495  cofsmo  8649  isf32lem10  8742  fin1a2lem7  8786  fodomb  8904  iunfo  8914  tskuni  9161  gruima  9180  gruen  9190  axpre-sup  9546  supcvg  13630  ruclem13  13836  imasval  14766  imasle  14778  imasaddfnlem  14783  imasaddflem  14785  imasvscafn  14792  imasvscaf  14794  imasless  14795  homadm  15225  homacd  15226  dmaf  15234  cdaf  15235  setcepi  15273  imasmnd2  15776  imasgrp2  15995  efgred2  16577  ghmcyg  16701  gsumval3OLD  16711  gsumval3  16714  gsumzoppg  16770  gsumzoppgOLD  16771  gsum2dlem2  16801  gsum2dOLD  16803  imasrng  17069  znunit  18397  znrrg  18399  cygznlem2a  18401  cygznlem3  18403  cncmp  19686  cnconn  19717  1stcfb  19740  dfac14  19882  qtopval2  19960  qtopuni  19966  qtopid  19969  qtopcld  19977  qtopcn  19978  qtopeu  19980  qtophmeo  20081  elfm3  20214  ovoliunnul  21681  uniiccdif  21750  dchrzrhcl  23276  lgsdchrval  23378  rpvmasumlem  23428  dchrmusum2  23435  dchrvmasumlem3  23440  dchrisum0ff  23448  dchrisum0flblem1  23449  rpvmasum2  23453  dchrisum0re  23454  dchrisum0lem2a  23458  fargshiftfo  24342  grpocl  24906  grporndm  24916  resgrprn  24986  subgores  25010  issubgoi  25016  ghgrplem2  25073  ghgrp  25074  rngosn  25110  rngodm1dm2  25124  rngosn3  25132  vafval  25200  smfval  25202  nvgf  25215  vsfval  25232  pjhf  26330  elunop  26495  unopf1o  26539  cnvunop  26541  pjinvari  26814  iunrdx  27132  fimacnvinrn  27176  xppreima  27187  qtophaus  27665  ghomfo  28534  ghomcl  28535  ghomgsg  28536  ghomf1olem  28537  bdaydm  29043  volsupnfl  29664  cocanfo  29839  exidreslem  29970