Theorem f1of 5500

Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of	|- ( F : A -1-1-onto-> B -> F : A --> B )

Proof of Theorem f1of

Step	Hyp	Ref	Expression
1		f1of1 5499	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5459	. 2 |- ( F : A -1-1-> B -> F : A --> B )
3	1, 2	syl 14	1 |- ( F : A -1-1-onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   -->wf 5250   -1-1->wf1 5251   -1-1-onto->wf1o 5253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-f1 5259  df-f1o 5261

This theorem is referenced by:  f1ofn  5501  f1oabexg  5512  f1ompt  5709  f1oresrab  5723  fsn  5730  fsnunf  5758  f1ocnvfv1  5820  f1ocnvfv2  5821  f1ocnvdm  5824  fcof1o  5832  isocnv  5854  isores2  5856  isotr  5859  isopolem  5865  isosolem  5867  f1oiso2  5870  f1ofveu  5906  smoiso  6355  mapsn  6744  f1oen2g  6809  en1  6853  enm  6874  mapen  6902  fidceq  6925  dif1en  6935  fin0  6941  fin0or  6942  ac6sfi  6954  en2eqpr  6963  fiintim  6985  isotilem  7065  supisoex  7068  supisoti  7069  ordiso2  7094  caseinl  7150  caseinr  7151  omp1eomlem  7153  ctm  7168  enomnilem  7197  enmkvlem  7220  enwomnilem  7228  cc3  7328  frecuzrdgg  10487  fnn0nninf  10509  fxnn0nninf  10510  0tonninf  10511  1tonninf  10512  iseqf1olemkle  10568  iseqf1olemklt  10569  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemmo  10576  iseqf1olemqk  10578  iseqf1olemjpcl  10579  iseqf1olemfvp  10581  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seq3f1olemstep  10585  seq3f1olemp  10586  seq3f1oleml  10587  seq3f1o  10588  seqf1oglem1  10590  seqf1oglem2  10591  seqf1og  10592  hashfz1  10854  omgadd  10873  hashfacen  10907  leisorel  10908  zfz1isolemiso  10910  seq3coll  10913  cnrecnv  11054  sumeq2  11502  summodclem3  11523  summodclem2a  11524  fsumgcl  11529  fsum3  11530  fsumf1o  11533  fisumss  11535  fsumcl2lem  11541  fsumadd  11549  fsummulc2  11591  prodeq2  11700  prodmodclem3  11718  prodmodclem2a  11719  fprodseq  11726  fprodf1o  11731  fprodssdc  11733  fprodmul  11734  nninfctlemfo  12177  sqpweven  12313  2sqpwodd  12314  phimullem  12363  eulerthlem1  12365  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  ennnfonelemjn  12559  ennnfonelemp1  12563  ennnfonelemhdmp1  12566  ennnfonelemss  12567  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemnn0  12579  ennnfonelemim  12581  ctinfomlemom  12584  ctiunctlemudc  12594  ctiunctlemfo  12596  ssnnctlemct  12603  idmhm  13041  mhmf1o  13042  idghm  13329  ghmf1o  13345  gsumfzreidx  13407  ssidcn  14378  txhmeo  14487  dvid  14847  dvexp  14860  dfrelog  14995  relogcl  14997  012of  15486  2o01f  15487  iswomninnlem  15539