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  11192  sumeq2  11641  summodclem3  11662  summodclem2a  11663  fsumgcl  11668  fsum3  11669  fsumf1o  11672  fisumss  11674  fsumcl2lem  11680  fsumadd  11688  fsummulc2  11730  prodeq2  11839  prodmodclem3  11857  prodmodclem2a  11858  fprodseq  11865  fprodf1o  11870  fprodssdc  11872  fprodmul  11873  nninfctlemfo  12332  sqpweven  12468  2sqpwodd  12469  phimullem  12518  eulerthlem1  12520  eulerthlemrprm  12522  eulerthlema  12523  eulerthlemh  12524  eulerthlemth  12525  ennnfonelemjn  12744  ennnfonelemp1  12748  ennnfonelemhdmp1  12751  ennnfonelemss  12752  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemex  12756  ennnfonelemnn0  12764  ennnfonelemim  12766  ctinfomlemom  12769  ctiunctlemudc  12779  ctiunctlemfo  12781  ssnnctlemct  12788  idmhm  13272  mhmf1o  13273  idghm  13566  ghmf1o  13582  gsumfzreidx  13644  psrnegcl  14416  psrlinv  14417  ssidcn  14653  txhmeo  14762  dvid  15138  dvidre  15140  dvexp  15154  dfrelog  15303  relogcl  15305  012of  15892  2o01f  15893  iswomninnlem  15950