MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fof Unicode version

Theorem fof 5800
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
fof

Proof of Theorem fof
StepHypRef Expression
1 eqimss 3555 . . 3
21anim2i 569 . 2
3 df-fo 5599 . 2
4 df-f 5597 . 2
52, 3, 43imtr4i 266 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  C_wss 3475  rancrn 5005  Fnwfn 5588  -->wf 5589  -onto->wfo 5591
This theorem is referenced by:  fofun  5801  fofn  5802  dffo2  5804  foima  5805  resdif  5841  fconst5  6128  fconstfvOLD  6134  cocan2  6195  foeqcnvco  6203  soisoi  6224  ffoss  6761  fornex  6769  algrflem  6909  tposf2  6998  smoiso2  7059  mapsn  7480  ssdomg  7581  fopwdom  7645  unfilem2  7805  fodomfib  7820  fofinf1o  7821  brwdomn0  8016  fowdom  8018  wdomtr  8022  wdomima2g  8033  fodomfi2  8462  wdomfil  8463  alephiso  8500  iunfictbso  8516  cofsmo  8670  isf32lem10  8763  fin1a2lem7  8807  fodomb  8925  iunfo  8935  tskuni  9182  gruima  9201  gruen  9211  axpre-sup  9567  supcvg  13667  ruclem13  13975  imasval  14908  imasle  14920  imasaddfnlem  14925  imasaddflem  14927  imasvscafn  14934  imasvscaf  14936  imasless  14937  homadm  15367  homacd  15368  dmaf  15376  cdaf  15377  setcepi  15415  imasmnd2  15957  imasgrp2  16185  mhmid  16191  mhmmnd  16192  mhmfmhm  16193  ghmgrp  16194  efgred2  16771  ghmfghm  16839  ghmcyg  16898  gsumval3OLD  16908  gsumval3  16911  gsumzoppg  16967  gsumzoppgOLD  16968  gsum2dlem2  16998  gsum2dOLD  17000  imasring  17268  znunit  18602  znrrg  18604  cygznlem2a  18606  cygznlem3  18608  cncmp  19892  cnconn  19923  1stcfb  19946  dfac14  20119  qtopval2  20197  qtopuni  20203  qtopid  20206  qtopcld  20214  qtopcn  20215  qtopeu  20217  qtophmeo  20318  elfm3  20451  ovoliunnul  21918  uniiccdif  21987  dchrzrhcl  23520  lgsdchrval  23622  rpvmasumlem  23672  dchrmusum2  23679  dchrvmasumlem3  23684  dchrisum0ff  23692  dchrisum0flblem1  23693  rpvmasum2  23697  dchrisum0re  23698  dchrisum0lem2a  23702  fargshiftfo  24638  grpocl  25202  grporndm  25212  resgrprn  25282  subgores  25306  issubgoi  25312  ghgrplem2OLD  25369  ghgrpOLD  25370  rngosn  25406  rngodm1dm2  25420  rngosn3  25428  vafval  25496  smfval  25498  nvgf  25511  vsfval  25528  pjhf  26626  elunop  26791  unopf1o  26835  cnvunop  26837  pjinvari  27110  foresf1o  27403  rabfodom  27404  iunrdx  27431  fimacnvinrn  27475  xppreima  27487  qtophaus  27839  mtyf  28912  ghomfo  29031  ghomcl  29032  ghomgsg  29033  ghomf1olem  29034  bdaydm  29438  volsupnfl  30059  cocanfo  30208  exidreslem  30339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-f 5597  df-fo 5599
  Copyright terms: Public domain W3C validator