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

Theorem f1f1orn 5646
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 5601 . 2
2 df-f1 5422 . . 3
32simprbi 452 . 2
4 f1orn 5645 . 2
51, 3, 4sylanbrc 647 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  `'ccnv 4843  rancrn 4845  Funwfun 5411  Fnwfn 5412  -->wf 5413  -1-1->wf1 5414  -1-1-onto->wf1o 5416
This theorem is referenced by:  f1ores  5649  f1cnv  5658  f1cocnv1  5664  f1ocnvfvrneq  5964  fnwelem  6644  oacomf1olem  6919  domss2  7378  ssenen  7393  sucdom2  7415  f1finf1o  7447  f1fi  7505  marypha1lem  7550  hartogslem1  7623  infdifsn  7723  infxpenlem  8009  infxpenc2lem1  8014  fseqenlem2  8020  ac10ct  8029  acndom  8046  acndom2  8049  dfac12lem2  8138  dfac12lem3  8139  fictb  8239  fin23lem21  8333  axcc2lem  8430  pwfseqlem1  8647  pwfseqlem5  8652  hashf1lem1  11995  hashf1lem2  11996  4sqlem11  13802  xpsff1o2  14287  yoniso  14873  imasmndf1  15237  imasgrpf1  15438  conjsubgen  15541  cayley  15615  odinf  15702  sylow1lem2  15736  sylow2blem1  15757  gsumval3  16017  dprdf1  16094  2ndcdisj  18023  dis2ndc  18027  qtopf1  18352  ovolicc2lem4  19920  itg1addlem4  20093  basellem3  21374  fsumvma  21506  dchrisum0fno1  21714  usgraf1o  21891  constr3trllem1  22146  constr3trllem5  22150  erdszelem10  25725  eldioph2lem2  27750  dnwech  28052  islindf3  28202  dihcnvcl  33342  dihcnvid1  33343  dihcnvid2  33344  dihlspsnat  33404  dihglblem6  33411  dochocss  33437  dochnoncon  33462  mapdcnvcl  33723  mapdcnvid2  33728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-in 3360  df-ss 3367  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424
  Copyright terms: Public domain W3C validator