Theorem f1of 5580

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 5579	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5539	. 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 5320   -1-1->wf1 5321   -1-1-onto->wf1o 5323

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 5329  df-f1o 5331

This theorem is referenced by:  f1ofn  5581  f1oabexg  5592  f1ompt  5794  f1oresrab  5808  fsn  5815  fsnunf  5849  f1ocnvfv1  5913  f1ocnvfv2  5914  f1ocnvdm  5917  fcof1o  5925  isocnv  5947  isores2  5949  isotr  5952  isopolem  5958  isosolem  5960  f1oiso2  5963  f1ofveu  6001  smoiso  6463  mapsn  6854  f1oen2g  6923  en1  6968  enm  6999  mapen  7027  fidceq  7051  dif1en  7061  fin0  7067  fin0or  7068  ac6sfi  7080  en2eqpr  7092  fiintim  7116  isotilem  7196  supisoex  7199  supisoti  7200  ordiso2  7225  caseinl  7281  caseinr  7282  omp1eomlem  7284  ctm  7299  enomnilem  7328  enmkvlem  7351  enwomnilem  7359  pr2cv1  7391  cc3  7477  frecuzrdgg  10668  fnn0nninf  10690  fxnn0nninf  10691  0tonninf  10692  1tonninf  10693  iseqf1olemkle  10749  iseqf1olemklt  10750  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemmo  10757  iseqf1olemqk  10759  iseqf1olemjpcl  10760  iseqf1olemfvp  10762  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seq3f1olemstep  10766  seq3f1olemp  10767  seq3f1oleml  10768  seq3f1o  10769  seqf1oglem1  10771  seqf1oglem2  10772  seqf1og  10773  hashfz1  11035  omgadd  11055  hashfacen  11090  leisorel  11091  zfz1isolemiso  11093  seq3coll  11096  cnrecnv  11461  sumeq2  11910  summodclem3  11931  summodclem2a  11932  fsumgcl  11937  fsum3  11938  fsumf1o  11941  fisumss  11943  fsumcl2lem  11949  fsumadd  11957  fsummulc2  11999  prodeq2  12108  prodmodclem3  12126  prodmodclem2a  12127  fprodseq  12134  fprodf1o  12139  fprodssdc  12141  fprodmul  12142  nninfctlemfo  12601  sqpweven  12737  2sqpwodd  12738  phimullem  12787  eulerthlem1  12789  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  ennnfonelemjn  13013  ennnfonelemp1  13017  ennnfonelemhdmp1  13020  ennnfonelemss  13021  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemex  13025  ennnfonelemnn0  13033  ennnfonelemim  13035  ctinfomlemom  13038  ctiunctlemudc  13048  ctiunctlemfo  13050  ssnnctlemct  13057  idmhm  13542  mhmf1o  13543  idghm  13836  ghmf1o  13852  gsumfzreidx  13914  psrnegcl  14687  psrlinv  14688  ssidcn  14924  txhmeo  15033  dvid  15409  dvidre  15411  dvexp  15425  dfrelog  15574  relogcl  15576  uspgriedgedg  16018  012of  16528  2o01f  16529  iswomninnlem  16589