Theorem f1of 5583

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 5582	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5542	. 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 5322   -1-1->wf1 5323   -1-1-onto->wf1o 5325

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

This theorem is referenced by:  f1ofn  5584  f1oabexg  5595  f1ompt  5798  f1oresrab  5812  fsn  5819  fsnunf  5854  f1ocnvfv1  5918  f1ocnvfv2  5919  f1ocnvdm  5922  fcof1o  5930  isocnv  5952  isores2  5954  isotr  5957  isopolem  5963  isosolem  5965  f1oiso2  5968  f1ofveu  6006  smoiso  6468  mapsn  6859  f1oen2g  6928  en1  6973  enm  7004  mapen  7032  fidceq  7056  dif1en  7068  fin0  7074  fin0or  7075  ac6sfi  7087  en2eqpr  7099  fiintim  7123  isotilem  7205  supisoex  7208  supisoti  7209  ordiso2  7234  caseinl  7290  caseinr  7291  omp1eomlem  7293  ctm  7308  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  pr2cv1  7400  cc3  7487  frecuzrdgg  10679  fnn0nninf  10701  fxnn0nninf  10702  0tonninf  10703  1tonninf  10704  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemmo  10768  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1olemp  10778  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  hashfz1  11046  omgadd  11066  hashfacen  11101  leisorel  11102  zfz1isolemiso  11104  seq3coll  11107  cnrecnv  11488  sumeq2  11937  summodclem3  11959  summodclem2a  11960  fsumgcl  11965  fsum3  11966  fsumf1o  11969  fisumss  11971  fsumcl2lem  11977  fsumadd  11985  fsummulc2  12027  prodeq2  12136  prodmodclem3  12154  prodmodclem2a  12155  fprodseq  12162  fprodf1o  12167  fprodssdc  12169  fprodmul  12170  nninfctlemfo  12629  sqpweven  12765  2sqpwodd  12766  phimullem  12815  eulerthlem1  12817  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  ennnfonelemjn  13041  ennnfonelemp1  13045  ennnfonelemhdmp1  13048  ennnfonelemss  13049  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemnn0  13061  ennnfonelemim  13063  ctinfomlemom  13066  ctiunctlemudc  13076  ctiunctlemfo  13078  ssnnctlemct  13085  idmhm  13570  mhmf1o  13571  idghm  13864  ghmf1o  13880  gsumfzreidx  13942  psrnegcl  14716  psrlinv  14717  ssidcn  14953  txhmeo  15062  dvid  15438  dvidre  15440  dvexp  15454  dfrelog  15603  relogcl  15605  uspgriedgedg  16049  012of  16643  2o01f  16644  iswomninnlem  16705  gfsumval  16732  gsumgfsumlem  16735  gfsump1  16738