Theorem f1of 5634

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 5633	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5593	. 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 5368   -1-1->wf1 5369   -1-1-onto->wf1o 5371

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 5377  df-f1o 5379

This theorem is referenced by:  f1ofn  5635  f1oabexg  5646  f1ompt  5850  f1oresrab  5864  fsn  5871  fsnunf  5906  f1ocnvfv1  5973  f1ocnvfv2  5974  f1ocnvdm  5977  fcof1o  5985  isocnv  6007  isores2  6009  isotr  6012  isopolem  6018  isosolem  6020  f1oiso2  6023  f1ofveu  6063  suppsnopdc  6480  smoiso  6563  mapsnd  6960  mapsn  6962  f1oen2g  7031  en1  7076  enm  7108  mapen  7136  fidceq  7161  dif1en  7173  fin0  7179  fin0or  7180  ac6sfi  7192  en2eqpr  7204  fiintim  7228  isotilem  7336  supisoex  7339  supisoti  7340  ordiso2  7365  caseinl  7421  caseinr  7422  omp1eomlem  7424  ctm  7439  enomnilem  7468  enmkvlem  7491  enwomnilem  7499  pr2cv1  7531  cc3  7624  frecuzrdgg  10831  fnn0nninf  10853  fxnn0nninf  10854  0tonninf  10855  1tonninf  10856  iseqf1olemkle  10912  iseqf1olemklt  10913  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemmo  10920  iseqf1olemqk  10922  iseqf1olemjpcl  10923  iseqf1olemfvp  10925  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  seq3f1olemstep  10929  seq3f1olemp  10930  seq3f1oleml  10931  seq3f1o  10932  seqf1oglem1  10934  seqf1oglem2  10935  seqf1og  10936  hashfz1  11200  omgadd  11220  hashfacen  11262  hashf1lem1  11263  leisorel  11267  zfz1isolemiso  11269  seq3coll  11272  cnrecnv  11654  sumeq2  12103  summodclem3  12125  summodclem2a  12126  fsumgcl  12131  fsum3  12132  fsumf1o  12135  fisumss  12137  fsumcl2lem  12143  fsumadd  12151  fsummulc2  12193  prodeq2  12302  prodmodclem3  12320  prodmodclem2a  12321  fprodseq  12328  fprodf1o  12333  fprodssdc  12335  fprodmul  12336  nninfctlemfo  12795  sqpweven  12931  2sqpwodd  12932  phimullem  12981  eulerthlem1  12983  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  ballotfilemsima  13237  ennnfonelemjn  13271  ennnfonelemp1  13275  ennnfonelemhdmp1  13278  ennnfonelemss  13279  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemnn0  13291  ennnfonelemim  13293  ctinfomlemom  13296  ctiunctlemudc  13306  ctiunctlemfo  13308  ssnnctlemct  13315  idmhm  13753  mhmf1o  13754  idghm  14039  ghmf1o  14055  gzsumreidx  14118  gzsumshift  14126  gsumvalfi  14129  gsump1  14134  gsumf1ofi  14137  gsummhmfi  14141  gsumressfi  14144  psrnegcl  14997  psrlinv  14998  ssidcn  15234  txhmeo  15343  dvid  15719  dvidre  15721  dvexp  15735  dfrelog  15884  relogcl  15886  uspgriedgedg  16334  012of  16937  2o01f  16938  iswomninnlem  17004