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

Theorem f1f1orn 5669
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 5624 . 2
2 df-f1 5443 . . 3
32simprbi 452 . 2
4 f1orn 5668 . 2
51, 3, 4sylanbrc 647 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  `'ccnv 4861  rancrn 4863  Funwfun 5432  Fnwfn 5433  -->wf 5434  -1-1->wf1 5435  -1-1-onto->wf1o 5437
This theorem is referenced by:  f1ores  5672  f1cnv  5681  f1cocnv1  5687  f1ocnvfvrneq  6000  fnwelem  6693  oacomf1olem  6969  domss2  7431  ssenen  7446  sucdom2  7468  f1finf1o  7500  f1fi  7559  marypha1lem  7605  hartogslem1  7678  infdifsn  7778  infxpenlem  8066  infxpenc2lem1  8071  fseqenlem2  8077  ac10ct  8086  acndom  8103  acndom2  8106  dfac12lem2  8195  dfac12lem3  8196  fictb  8296  fin23lem21  8390  axcc2lem  8487  pwfseqlem1  8704  pwfseqlem5  8709  hashf1lem1  12055  hashf1lem2  12056  4sqlem11  13863  xpsff1o2  14350  yoniso  14936  imasmndf1  15300  imasgrpf1  15506  conjsubgen  15609  cayley  15695  odinf  15808  sylow1lem2  15842  sylow2blem1  15863  gsumval3  16124  dprdf1  16206  2ndcdisj  18534  dis2ndc  18538  qtopf1  18863  ovolicc2lem4  20431  itg1addlem4  20604  basellem3  21886  fsumvma  22018  dchrisum0fno1  22226  usgraf1o  22403  constr3trllem1  22658  constr3trllem5  22662  erdszelem10  26234  eldioph2lem2  28247  dnwech  28549  islindf3  28636  dihcnvcl  33619  dihcnvid1  33620  dihcnvid2  33621  dihlspsnat  33681  dihglblem6  33688  dochocss  33714  dochnoncon  33739  mapdcnvcl  34000  mapdcnvid2  34005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-in 3372  df-ss 3379  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445
  Copyright terms: Public domain W3C validator