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

Theorem f1ores 5835
Description: The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by NM, 25-Mar-1998.)
Assertion
Ref Expression
f1ores

Proof of Theorem f1ores
StepHypRef Expression
1 f1ssres 5793 . . 3
2 f1f1orn 5832 . . 3
31, 2syl 16 . 2
4 df-ima 5017 . . 3
5 f1oeq3 5814 . . 3
64, 5ax-mp 5 . 2
73, 6sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  C_wss 3475  rancrn 5005  |`cres 5006  "cima 5007  -1-1->wf1 5590  -1-1-onto->wf1o 5592
This theorem is referenced by:  f1imacnv  5837  f1oresrab  6063  isores3  6231  isoini2  6235  f1imaeng  7595  f1imaen2g  7596  domunsncan  7637  php3  7723  ssfi  7760  infdifsn  8094  infxpenlem  8412  ackbij2lem2  8641  fin1a2lem6  8806  grothomex  9228  fsumss  13547  ackbijnn  13640  fprodss  13755  unbenlem  14426  eqgen  16254  symgfixelsi  16460  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3lem2  16910  gsumzaddlem  16934  gsumzaddlemOLD  16936  coe1mul2lem2  18309  lindsmm  18863  tsmsf1o  20647  ovoliunlem1  21913  dvcnvrelem2  22419  logf1o2  23031  dvlog  23032  eupares  24975  adjbd1o  27004  rinvf1o  27472  indf1ofs  28039  eulerpartgbij  28311  eulerpartlemgh  28317  ballotlemfrc  28465  erdsze2lem2  28648  ismtyres  30304  pwfi2f1o  31044
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-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600
  Copyright terms: Public domain W3C validator