Theorem f1of 5619

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 5618	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5578	. 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 5353   -1-1->wf1 5354   -1-1-onto->wf1o 5356

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 5362  df-f1o 5364

This theorem is referenced by:  f1ofn  5620  f1oabexg  5631  f1ompt  5833  f1oresrab  5847  fsn  5854  fsnunf  5889  f1ocnvfv1  5956  f1ocnvfv2  5957  f1ocnvdm  5960  fcof1o  5968  isocnv  5990  isores2  5992  isotr  5995  isopolem  6001  isosolem  6003  f1oiso2  6006  f1ofveu  6046  suppsnopdc  6463  smoiso  6546  mapsnd  6936  mapsn  6938  f1oen2g  7007  en1  7052  enm  7084  mapen  7112  fidceq  7137  dif1en  7149  fin0  7155  fin0or  7156  ac6sfi  7168  en2eqpr  7180  fiintim  7204  isotilem  7310  supisoex  7313  supisoti  7314  ordiso2  7339  caseinl  7395  caseinr  7396  omp1eomlem  7398  ctm  7413  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  pr2cv1  7505  cc3  7598  frecuzrdgg  10802  fnn0nninf  10824  fxnn0nninf  10825  0tonninf  10826  1tonninf  10827  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemmo  10891  iseqf1olemqk  10893  iseqf1olemjpcl  10894  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1olemstep  10900  seq3f1olemp  10901  seq3f1oleml  10902  seq3f1o  10903  seqf1oglem1  10905  seqf1oglem2  10906  seqf1og  10907  hashfz1  11171  omgadd  11191  hashfacen  11233  leisorel  11234  zfz1isolemiso  11236  seq3coll  11239  cnrecnv  11620  sumeq2  12069  summodclem3  12091  summodclem2a  12092  fsumgcl  12097  fsum3  12098  fsumf1o  12101  fisumss  12103  fsumcl2lem  12109  fsumadd  12117  fsummulc2  12159  prodeq2  12268  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  fprodf1o  12299  fprodssdc  12301  fprodmul  12302  nninfctlemfo  12761  sqpweven  12897  2sqpwodd  12898  phimullem  12947  eulerthlem1  12949  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  ballotfilemsima  13203  ennnfonelemjn  13237  ennnfonelemp1  13241  ennnfonelemhdmp1  13244  ennnfonelemss  13245  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemnn0  13257  ennnfonelemim  13259  ctinfomlemom  13262  ctiunctlemudc  13272  ctiunctlemfo  13274  ssnnctlemct  13281  idmhm  13724  mhmf1o  13725  idghm  14012  ghmf1o  14028  gsumfzreidx  14090  gfsumval  14102  gsumshift  14105  gfsump1  14108  psrnegcl  14964  psrlinv  14965  ssidcn  15201  txhmeo  15310  dvid  15686  dvidre  15688  dvexp  15702  dfrelog  15851  relogcl  15853  uspgriedgedg  16300  012of  16893  2o01f  16894  iswomninnlem  16960