Theorem f1of 5539

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 5538	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5498	. 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 5281   -1-1->wf1 5282   -1-1-onto->wf1o 5284

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 5290  df-f1o 5292

This theorem is referenced by:  f1ofn  5540  f1oabexg  5551  f1ompt  5749  f1oresrab  5763  fsn  5770  fsnunf  5802  f1ocnvfv1  5864  f1ocnvfv2  5865  f1ocnvdm  5868  fcof1o  5876  isocnv  5898  isores2  5900  isotr  5903  isopolem  5909  isosolem  5911  f1oiso2  5914  f1ofveu  5950  smoiso  6406  mapsn  6795  f1oen2g  6864  en1  6909  enm  6935  mapen  6963  fidceq  6987  dif1en  6997  fin0  7003  fin0or  7004  ac6sfi  7016  en2eqpr  7025  fiintim  7049  isotilem  7129  supisoex  7132  supisoti  7133  ordiso2  7158  caseinl  7214  caseinr  7215  omp1eomlem  7217  ctm  7232  enomnilem  7261  enmkvlem  7284  enwomnilem  7292  pr2cv1  7324  cc3  7410  frecuzrdgg  10593  fnn0nninf  10615  fxnn0nninf  10616  0tonninf  10617  1tonninf  10618  iseqf1olemkle  10674  iseqf1olemklt  10675  iseqf1olemqcl  10676  iseqf1olemnab  10678  iseqf1olemmo  10682  iseqf1olemqk  10684  iseqf1olemjpcl  10685  iseqf1olemfvp  10687  seq3f1olemqsumkj  10688  seq3f1olemqsumk  10689  seq3f1olemqsum  10690  seq3f1olemstep  10691  seq3f1olemp  10692  seq3f1oleml  10693  seq3f1o  10694  seqf1oglem1  10696  seqf1oglem2  10697  seqf1og  10698  hashfz1  10960  omgadd  10979  hashfacen  11013  leisorel  11014  zfz1isolemiso  11016  seq3coll  11019  cnrecnv  11306  sumeq2  11755  summodclem3  11776  summodclem2a  11777  fsumgcl  11782  fsum3  11783  fsumf1o  11786  fisumss  11788  fsumcl2lem  11794  fsumadd  11802  fsummulc2  11844  prodeq2  11953  prodmodclem3  11971  prodmodclem2a  11972  fprodseq  11979  fprodf1o  11984  fprodssdc  11986  fprodmul  11987  nninfctlemfo  12446  sqpweven  12582  2sqpwodd  12583  phimullem  12632  eulerthlem1  12634  eulerthlemrprm  12636  eulerthlema  12637  eulerthlemh  12638  eulerthlemth  12639  ennnfonelemjn  12858  ennnfonelemp1  12862  ennnfonelemhdmp1  12865  ennnfonelemss  12866  ennnfonelemkh  12868  ennnfonelemhf1o  12869  ennnfonelemex  12870  ennnfonelemnn0  12878  ennnfonelemim  12880  ctinfomlemom  12883  ctiunctlemudc  12893  ctiunctlemfo  12895  ssnnctlemct  12902  idmhm  13386  mhmf1o  13387  idghm  13680  ghmf1o  13696  gsumfzreidx  13758  psrnegcl  14530  psrlinv  14531  ssidcn  14767  txhmeo  14876  dvid  15252  dvidre  15254  dvexp  15268  dfrelog  15417  relogcl  15419  012of  16100  2o01f  16101  iswomninnlem  16160