Theorem f1f1orn 5832

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

Step	Hyp	Ref	Expression
1		f1fn 5787	. 2
2		df-f1 5598	. . 3
3	2	simprbi 464	. 2
4		f1orn 5831	. 2
5	1, 3, 4	sylanbrc 664	1

Syntax hints:  ->wi 4  `'ccnv 5003  rancrn 5005  Funwfun 5587  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  -1-1-onto->wf1o 5592

This theorem is referenced by:  f1ores  5835  f1cnv  5844  f1cocnv1  5850  f1ocnvfvrneq  6189  fnwelem  6915  oacomf1olem  7232  domss2  7696  ssenen  7711  sucdom2  7734  f1finf1o  7766  f1fi  7827  marypha1lem  7913  hartogslem1  7988  infdifsn  8094  infxpenlem  8412  infxpenc2lem1  8417  fseqenlem2  8427  ac10ct  8436  acndom  8453  acndom2  8456  dfac12lem2  8545  dfac12lem3  8546  fictb  8646  fin23lem21  8740  axcc2lem  8837  pwfseqlem1  9057  pwfseqlem5  9062  hashf1lem1  12504  hashf1lem2  12505  4sqlem11  14473  xpsff1o2  14968  yoniso  15554  imasmndf1  15959  imasgrpf1  16187  conjsubgen  16299  cayley  16439  odinf  16585  sylow1lem2  16619  sylow2blem1  16640  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3lem2  16910  gsumval3  16911  dprdf1  17080  islindf3  18861  uvcf1o  18881  2ndcdisj  19957  dis2ndc  19961  qtopf1  20317  ovolicc2lem4  21931  itg1addlem4  22106  basellem3  23356  fsumvma  23488  dchrisum0fno1  23696  usgraf1o  24358  uslgraf1oedg  24359  constr3trllem1  24650  constr3trllem5  24654  erdszelem10  28644  mrsubff1o  28875  msubff1o  28917  eldioph2lem2  30694  dnwech  30994  f1dmvrnfibi  32312  aacllem  33216  dihcnvcl  36998  dihcnvid1  36999  dihcnvid2  37000  dihlspsnat  37060  dihglblem6  37067  dochocss  37093  dochnoncon  37118  mapdcnvcl  37379  mapdcnvid2  37384

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-3an 975  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-f1 5598  df-fo 5599  df-f1o 5600