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  5853  f1ocnvfv1  5917  f1ocnvfv2  5918  f1ocnvdm  5921  fcof1o  5929  isocnv  5951  isores2  5953  isotr  5956  isopolem  5962  isosolem  5964  f1oiso2  5967  f1ofveu  6005  smoiso  6467  mapsn  6858  f1oen2g  6927  en1  6972  enm  7003  mapen  7031  fidceq  7055  dif1en  7067  fin0  7073  fin0or  7074  ac6sfi  7086  en2eqpr  7098  fiintim  7122  isotilem  7204  supisoex  7207  supisoti  7208  ordiso2  7233  caseinl  7289  caseinr  7290  omp1eomlem  7292  ctm  7307  enomnilem  7336  enmkvlem  7359  enwomnilem  7367  pr2cv1  7399  cc3  7486  frecuzrdgg  10677  fnn0nninf  10699  fxnn0nninf  10700  0tonninf  10701  1tonninf  10702  iseqf1olemkle  10758  iseqf1olemklt  10759  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemmo  10766  iseqf1olemqk  10768  iseqf1olemjpcl  10769  iseqf1olemfvp  10771  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seq3f1olemstep  10775  seq3f1olemp  10776  seq3f1oleml  10777  seq3f1o  10778  seqf1oglem1  10780  seqf1oglem2  10781  seqf1og  10782  hashfz1  11044  omgadd  11064  hashfacen  11099  leisorel  11100  zfz1isolemiso  11102  seq3coll  11105  cnrecnv  11470  sumeq2  11919  summodclem3  11940  summodclem2a  11941  fsumgcl  11946  fsum3  11947  fsumf1o  11950  fisumss  11952  fsumcl2lem  11958  fsumadd  11966  fsummulc2  12008  prodeq2  12117  prodmodclem3  12135  prodmodclem2a  12136  fprodseq  12143  fprodf1o  12148  fprodssdc  12150  fprodmul  12151  nninfctlemfo  12610  sqpweven  12746  2sqpwodd  12747  phimullem  12796  eulerthlem1  12798  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  ennnfonelemjn  13022  ennnfonelemp1  13026  ennnfonelemhdmp1  13029  ennnfonelemss  13030  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemnn0  13042  ennnfonelemim  13044  ctinfomlemom  13047  ctiunctlemudc  13057  ctiunctlemfo  13059  ssnnctlemct  13066  idmhm  13551  mhmf1o  13552  idghm  13845  ghmf1o  13861  gsumfzreidx  13923  psrnegcl  14696  psrlinv  14697  ssidcn  14933  txhmeo  15042  dvid  15418  dvidre  15420  dvexp  15434  dfrelog  15583  relogcl  15585  uspgriedgedg  16029  012of  16592  2o01f  16593  iswomninnlem  16653  gfsumval  16680  gsumgfsumlem  16683