Theorem fof 5612

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 3360	. . 3 |- ( ran F = B -> ran F C_ B )
2	1	anim2i 553	. 2 |- ( ( F Fn A /\ ran F = B ) -> ( F Fn A /\ ran F C_ B ) )
3		df-fo 5419	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5417	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5	2, 3, 4	3imtr4i 258	1 |- ( F : A -onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   C_ wss 3280   ran crn 4838   Fn wfn 5408   -->wf 5409   -onto->wfo 5411

This theorem is referenced by:  fofun  5613  fofn  5614  dffo2  5616  foima  5617  resdif  5655  ffoss  5666  fconst5  5908  fconstfv  5913  fornex  5929  cocan2  5984  foeqcnvco  5986  soisoi  6007  algrflem  6414  tposf2  6462  smoiso2  6590  mapsn  7014  ssdomg  7112  fopwdom  7175  unfilem2  7331  fodomfib  7345  fofinf1o  7346  brwdomn0  7493  fowdom  7495  wdomtr  7499  wdomima2g  7510  fodomfi2  7897  wdomfil  7898  alephiso  7935  iunfictbso  7951  cofsmo  8105  isf32lem10  8198  fin1a2lem7  8242  fodomb  8360  iunfo  8370  tskuni  8614  gruima  8633  gruen  8643  axpre-sup  9000  supcvg  12590  ruclem13  12796  imasval  13692  imasle  13703  imasaddfnlem  13708  imasaddflem  13710  imasvscafn  13717  imasvscaf  13719  imasless  13720  homadm  14150  homacd  14151  dmaf  14159  cdaf  14160  setcepi  14198  imasmnd2  14687  imasgrp2  14888  efgred2  15340  ghmcyg  15460  gsumval3  15469  gsumzoppg  15494  gsum2d  15501  imasrng  15680  znunit  16799  znrrg  16801  cygznlem2a  16803  cygznlem3  16805  cncmp  17409  cnconn  17438  1stcfb  17461  dfac14  17603  qtopval2  17681  qtopuni  17687  qtopid  17690  qtopcld  17698  qtopcn  17699  qtopeu  17701  qtophmeo  17802  elfm3  17935  ovoliunnul  19356  uniiccdif  19423  dchrzrhcl  20982  lgsdchrval  21084  rpvmasumlem  21134  dchrmusum2  21141  dchrvmasumlem3  21146  dchrisum0ff  21154  dchrisum0flblem1  21155  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem2a  21164  fargshiftfo  21578  grpocl  21741  grporndm  21751  resgrprn  21821  subgores  21845  issubgoi  21851  ghgrplem2  21908  ghgrp  21909  rngosn  21945  rngodm1dm2  21959  rngosn3  21967  vafval  22035  smfval  22037  nvgf  22050  vsfval  22067  pjhf  23163  elunop  23328  unopf1o  23372  cnvunop  23374  pjinvari  23647  iunrdx  23967  fimacnvinrn  24000  xppreima  24012  ghomfo  25055  ghomcl  25056  ghomgsg  25057  ghomf1olem  25058  bdaydm  25546  volsupnfl  26150  cocanfo  26309  exidreslem  26442

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294  df-f 5417  df-fo 5419