Theorem f1of 5521

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 5520	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5480	. 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 5266   -1-1->wf1 5267   -1-1-onto->wf1o 5269

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 5275  df-f1o 5277

This theorem is referenced by:  f1ofn  5522  f1oabexg  5533  f1ompt  5730  f1oresrab  5744  fsn  5751  fsnunf  5783  f1ocnvfv1  5845  f1ocnvfv2  5846  f1ocnvdm  5849  fcof1o  5857  isocnv  5879  isores2  5881  isotr  5884  isopolem  5890  isosolem  5892  f1oiso2  5895  f1ofveu  5931  smoiso  6387  mapsn  6776  f1oen2g  6845  en1  6890  enm  6914  mapen  6942  fidceq  6965  dif1en  6975  fin0  6981  fin0or  6982  ac6sfi  6994  en2eqpr  7003  fiintim  7027  isotilem  7107  supisoex  7110  supisoti  7111  ordiso2  7136  caseinl  7192  caseinr  7193  omp1eomlem  7195  ctm  7210  enomnilem  7239  enmkvlem  7262  enwomnilem  7270  cc3  7379  frecuzrdgg  10559  fnn0nninf  10581  fxnn0nninf  10582  0tonninf  10583  1tonninf  10584  iseqf1olemkle  10640  iseqf1olemklt  10641  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemmo  10648  iseqf1olemqk  10650  iseqf1olemjpcl  10651  iseqf1olemfvp  10653  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemqsum  10656  seq3f1olemstep  10657  seq3f1olemp  10658  seq3f1oleml  10659  seq3f1o  10660  seqf1oglem1  10662  seqf1oglem2  10663  seqf1og  10664  hashfz1  10926  omgadd  10945  hashfacen  10979  leisorel  10980  zfz1isolemiso  10982  seq3coll  10985  cnrecnv  11163  sumeq2  11612  summodclem3  11633  summodclem2a  11634  fsumgcl  11639  fsum3  11640  fsumf1o  11643  fisumss  11645  fsumcl2lem  11651  fsumadd  11659  fsummulc2  11701  prodeq2  11810  prodmodclem3  11828  prodmodclem2a  11829  fprodseq  11836  fprodf1o  11841  fprodssdc  11843  fprodmul  11844  nninfctlemfo  12303  sqpweven  12439  2sqpwodd  12440  phimullem  12489  eulerthlem1  12491  eulerthlemrprm  12493  eulerthlema  12494  eulerthlemh  12495  eulerthlemth  12496  ennnfonelemjn  12715  ennnfonelemp1  12719  ennnfonelemhdmp1  12722  ennnfonelemss  12723  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemex  12727  ennnfonelemnn0  12735  ennnfonelemim  12737  ctinfomlemom  12740  ctiunctlemudc  12750  ctiunctlemfo  12752  ssnnctlemct  12759  idmhm  13243  mhmf1o  13244  idghm  13537  ghmf1o  13553  gsumfzreidx  13615  psrnegcl  14387  psrlinv  14388  ssidcn  14624  txhmeo  14733  dvid  15109  dvidre  15111  dvexp  15125  dfrelog  15274  relogcl  15276  012of  15863  2o01f  15864  iswomninnlem  15921