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

Theorem f1f1orn 5732
Description: A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.)
Assertion
Ref Expression
f1f1orn

Proof of Theorem f1f1orn
StepHypRef Expression
1 f1fn 5687 . 2
2 df-f1 5506 . . 3
32simprbi 452 . 2
4 f1orn 5731 . 2
51, 3, 4sylanbrc 647 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  `'ccnv 4918  rancrn 4920  Funwfun 5495  Fnwfn 5496  -->wf 5497  -1-1->wf1 5498  -1-1-onto->wf1o 5500
This theorem is referenced by:  f1ores  5736  f1cnv  5746  f1cocnv1  5752  f1ocnvfvrneq  6067  fnwelem  6511  oacomf1olem  6856  domss2  7315  ssenen  7330  sucdom2  7352  f1finf1o  7384  f1fi  7442  marypha1lem  7487  hartogslem1  7560  infdifsn  7660  infxpenlem  7946  infxpenc2lem1  7951  fseqenlem2  7957  ac10ct  7966  acndom  7983  acndom2  7986  dfac12lem2  8075  dfac12lem3  8076  fictb  8176  fin23lem21  8270  axcc2lem  8367  pwfseqlem1  8584  pwfseqlem5  8589  hashf1lem1  11755  hashf1lem2  11756  4sqlem11  13374  xpsff1o2  13847  yoniso  14433  imasmndf1  14785  imasgrpf1  14986  conjsubgen  15089  cayley  15163  odinf  15250  sylow1lem2  15284  sylow2blem1  15305  gsumval3  15565  dprdf1  15642  2ndcdisj  17570  dis2ndc  17574  qtopf1  17899  ovolicc2lem4  19467  itg1addlem4  19640  basellem3  20916  fsumvma  21048  dchrisum0fno1  21256  usgraf1o  21433  constr3trllem1  21688  constr3trllem5  21692  erdszelem10  24990  eldioph2lem2  27000  dnwech  27302  islindf3  27452  dihcnvcl  32309  dihcnvid1  32310  dihcnvid2  32311  dihlspsnat  32371  dihglblem6  32378  dochocss  32404  dochnoncon  32429  mapdcnvcl  32690  mapdcnvid2  32695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3316  df-ss 3323  df-f 5505  df-f1 5506  df-fo 5507  df-f1o 5508
  Copyright terms: Public domain W3C validator