Theorem fof 5801

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 3513	. . 3 |- ( ran F = B -> ran F C_ B )
2	1	anim2i 571	. 2 |- ( ( F Fn A /\ ran F = B ) -> ( F Fn A /\ ran F C_ B ) )
3		df-fo 5598	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5596	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5	2, 3, 4	3imtr4i 269	1 |- ( F : A -onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   C_ wss 3433   ran crn 4846   Fn wfn 5587   -->wf 5588   -onto->wfo 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447  df-f 5596  df-fo 5598

This theorem is referenced by:  fofun  5802  fofn  5803  dffo2  5805  foima  5806  resdif  5842  fconst5  6128  fconstfvOLD  6133  cocan2  6196  foeqcnvco  6204  soisoi  6225  ffoss  6759  fornex  6767  algrflem  6907  tposf2  6996  smoiso2  7087  mapsn  7512  ssdomg  7613  fopwdom  7677  unfilem2  7833  fodomfib  7848  fofinf1o  7849  brwdomn0  8075  fowdom  8077  wdomtr  8081  wdomima2g  8092  fodomfi2  8480  wdomfil  8481  alephiso  8518  iunfictbso  8534  cofsmo  8688  isf32lem10  8781  fin1a2lem7  8825  fodomb  8943  iunfo  8953  tskuni  9197  gruima  9216  gruen  9226  axpre-sup  9582  supcvg  13881  ruclem13  14261  imasval  15361  imasle  15373  imasaddfnlem  15378  imasaddflem  15380  imasvscafn  15387  imasvscaf  15389  imasless  15390  homadm  15879  homacd  15880  dmaf  15888  cdaf  15889  setcepi  15927  imasmnd2  16517  imasgrp2  16745  mhmid  16751  mhmmnd  16752  mhmfmhm  16753  ghmgrp  16754  efgred2  17331  ghmfghm  17399  ghmcyg  17458  gsumval3  17469  gsumzoppg  17505  gsum2dlem2  17531  imasring  17775  znunit  19058  znrrg  19060  cygznlem2a  19062  cygznlem3  19064  cncmp  20331  cnconn  20361  1stcfb  20384  dfac14  20557  qtopval2  20635  qtopuni  20641  qtopid  20644  qtopcld  20652  qtopcn  20653  qtopeu  20655  qtophmeo  20756  elfm3  20889  ovoliunnul  22334  uniiccdif  22409  dchrzrhcl  24033  lgsdchrval  24135  rpvmasumlem  24185  dchrmusum2  24192  dchrvmasumlem3  24197  dchrisum0ff  24205  dchrisum0flblem1  24206  rpvmasum2  24210  dchrisum0re  24211  dchrisum0lem2a  24215  fargshiftfo  25208  grpocl  25770  grporndm  25780  resgrprn  25850  subgores  25874  issubgoi  25880  ghgrplem2OLD  25937  ghgrpOLD  25938  rngosn  25974  rngodm1dm2  25988  rngosn3  25996  vafval  26064  smfval  26066  nvgf  26079  vsfval  26096  pjhf  27193  elunop  27357  unopf1o  27401  cnvunop  27403  pjinvari  27676  foresf1o  27972  rabfodom  27973  iunrdx  28015  fimacnvinrn  28072  xppreima  28085  qtophaus  28499  sigapildsys  28820  carsgclctunlem3  28978  mtyf  29975  ghomfo  30094  ghomcl  30095  ghomgsg  30096  ghomf1olem  30097  bdaydm  30349  poimirlem26  31670  poimirlem27  31671  volsupnfl  31689  cocanfo  31748  exidreslem  31879  founiiun  37073  founiiun0  37092  sge0fodjrnlem  37796  ismeannd  37818  caragenunicl  37858