Theorem f1of 6378

Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem f1of

Step	Hyp	Ref	Expression
1		f1of1 6377	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 6338	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 6119  –1-1→wf1 6120  –1-1-onto→wf1o 6122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-an 387  df-f1 6128  df-f1o 6130

This theorem is referenced by:  f1ofn  6379  f1ompt  6630  f1oresrab  6644  fsn  6652  fsnunf  6707  f1ocnvfv1  6787  f1ocnvfv2  6788  fsnex  6793  f1ocnvdm  6795  fcof1oinvd  6803  fveqf1o  6812  isocnv  6835  isocnv3  6837  isores2  6838  isotr  6841  isofr2  6849  isopolem  6850  isosolem  6852  f1oiso2  6857  weniso  6859  f1ofveu  6900  f1oexrnex  7377  f1oabexg  7387  wemoiso  7413  suppsnop  7573  smoiso  7725  mapsnd  8164  ralxpmap  8174  f1oen2g  8239  en1  8289  enfixsn  8338  mapen  8393  ac6sfi  8473  domunfican  8502  fiint  8506  mapfienlem1  8579  mapfienlem2  8580  mapfienlem3  8581  mapfien  8582  supisoex  8649  supiso  8650  ordiso2  8689  ordtypelem10  8701  hartogslem1  8716  unxpwdom2  8762  cantnfle  8845  cantnfp1lem3  8854  cantnflem1b  8860  cantnflem1d  8862  cantnflem1  8863  cnfcomlem  8873  cnfcom  8874  cnfcom2lem  8875  cnfcom2  8876  cnfcom3lem  8877  cnfcom3  8878  cnfcom3clem  8879  djuin  9057  infxpenlem  9149  infxpenc  9154  infxpenc2lem2  9156  fseqenlem1  9160  acndom  9187  acndom2  9190  infpwfien  9198  iunfictbso  9250  infmap2  9355  ackbij2lem2  9377  infpssrlem3  9442  infpssrlem4  9443  fin23lem30  9479  isf32lem6  9495  isf32lem7  9496  isf32lem8  9497  enfin1ai  9521  axcc3  9575  axcclem  9594  ttukeylem7  9652  fpwwe2lem6  9772  fpwwe2lem7  9773  fpwwe2lem9  9775  canthp1lem2  9790  canthp1  9791  pwfseqlem4a  9798  pwfseqlem5  9800  dfle2  12266  axdc4uzlem  13077  seqf1olem1  13134  seqf1olem2  13135  seqf1o  13136  hashkf  13412  hasheqf1oi  13432  hasheqf1od  13434  hashcl  13437  hashgadd  13456  hashfacen  13527  hashf1lem1  13528  fz1isolem  13534  seqcoll  13537  seqcoll2  13538  cnrecnv  14282  sumeq2ii  14800  summolem3  14822  summolem2a  14823  fsum  14828  fsumf1o  14831  fsumss  14833  fsumcl2lem  14839  fsumadd  14847  fsummulc2  14890  fsumrelem  14913  ackbijnn  14934  prodeq2ii  15016  prodmolem3  15036  prodmolem2a  15037  fprod  15044  fprodf1o  15049  fprodss  15051  fprodser  15052  fprodcl2lem  15053  fprodmul  15063  fproddiv  15064  fprodn0  15082  fproddvdsd  15433  sadcaddlem  15552  sadadd2lem  15554  sadadd3  15556  sadaddlem  15561  sadasslem  15565  sadeq  15567  phimullem  15855  eulerthlem1  15857  eulerthlem2  15858  unbenlem  15983  vdwlem8  16063  0ram  16095  wunndx  16243  xpsaddlem  16588  xpsvsca  16592  xpsle  16594  idfucl  16893  setccatid  17086  setcinv  17092  catcisolem  17108  estrccatid  17124  funcestrcsetclem7  17139  funcestrcsetclem8  17140  funcsetcestrclem7  17154  funcsetcestrclem8  17155  yonffthlem  17275  gsumpropd2lem  17626  idmhm  17697  mhmf1o  17698  gsumws1  17729  idghm  18026  ghmf1o  18041  symgval  18149  symgbas  18150  elsymgbas  18152  symgbasf  18154  symgbasfi  18156  symg1bas  18166  symggrp  18170  symgid  18171  lactghmga  18174  symgfixf1  18207  f1omvdmvd  18213  f1omvdconj  18216  f1omvdco2  18218  pmtrfconj  18236  symggen  18240  pmtrdifellem1  18246  pmtrdifellem2  18247  psgnunilem1  18263  gsumval3eu  18658  gsumval3lem1  18659  gsumval3  18661  gsumzf1o  18666  gsumconst  18687  gsumsub  18701  gsumcom2  18727  dprdfsub  18774  dprdf1o  18785  dprdsn  18789  ablfaclem2  18839  srngcl  19211  lmhmf1o  19405  fidomndrnglem  19667  psrass1lem  19738  psrnegcl  19757  psrlinv  19758  coe1f2  19939  coe1add  19994  evls1rhmlem  20046  evl1sca  20058  pf1ind  20079  gsumfsum  20173  zntoslem  20264  islinds2  20519  lindsmm  20534  mat1dimelbas  20645  mat1f  20656  mdetleib2  20762  mdetrsca  20777  mdetralt  20782  mdetunilem7  20792  mdetunilem9  20794  ssidcn  21430  hmphdis  21970  indishmph  21972  cmphaushmeo  21974  ordthmeolem  21975  txhmeo  21977  qtopf1  21990  ufldom  22136  symgtgp  22275  tsmsf1o  22318  iducn  22457  imasdsf1olem  22548  xpsdsval  22556  imasf1obl  22663  icchmeo  23110  iccpnfcnv  23113  xrhmeo  23115  cnheiborlem  23123  ovolctb  23656  ovoliunlem1  23668  ovoliunlem2  23669  iunmbl2  23723  dyadmbl  23766  vitalilem2  23775  vitalilem3  23776  vitalilem4  23777  vitalilem5  23778  mbfid  23801  dvid  24080  dvexp  24115  dvcnvlem  24138  dvcnv  24139  dvcnvrelem2  24180  dvcnvre  24181  efcvx  24602  reefgim  24603  efif1olem4  24691  eff1olem  24694  logrncl  24713  relogcl  24721  dvrelog  24782  relogcn  24783  logcn  24792  logf1o2  24795  dvlog  24796  dvlog2  24798  advlog  24799  advlogexp  24800  logtayl  24805  logccv  24808  dvcxp1  24883  loglesqrt  24901  asinrebnd  25041  dvatan  25075  efrlim  25109  amgmlem  25129  lgamcvg2  25194  wilthlem2  25208  wilthlem3  25209  sqff1o  25321  lgsqrlem4  25487  logdivsum  25635  log2sumbnd  25646  isismt  25846  motcl  25851  motco  25852  cnvmot  25853  motgrp  25855  motcgrg  25856  f1otrg  26170  f1otrge  26171  axlowdimlem10  26250  axcontlem5  26267  axcontlem10  26272  upgrres1  26610  umgrres1  26611  upgriseupth  27572  pliguhgr  27885  dmadjrn  29298  unopnorm  29320  unopadj  29322  unoplin  29323  counop  29324  idcnop  29384  idhmop  29385  unopbd  29418  bracnln  29512  cnvbraval  29513  leopnmid  29541  nmopleid  29542  hmopidmch  29556  hmopidmpj  29557  disjrdx  29940  fmptco1f1o  29972  isoun  30016  padct  30034  fcobij  30037  fcobijfs  30038  abliso  30230  symgfcoeu  30379  tpr2rico  30492  xrge0iifmhm  30519  xrge0pluscn  30520  rrhre  30599  esumf1o  30646  volmeas  30828  eulerpartgbij  30968  eulerpartlemmf  30971  eulerpartlemgvv  30972  eulerpartlemgf  30975  eulerpartlemgs2  30976  eulerpartlemn  30977  ballotlemsima  31112  reprpmtf1o  31242  logdivsqrle  31266  hgt750lemg  31270  deranglem  31683  derangsn  31687  derangenlem  31688  subfacp1lem4  31700  subfacp1lem5  31701  subfacp1lem6  31702  cvmfolem  31796  cvmliftlem6  31807  poimirlem1  33947  poimirlem2  33948  poimirlem3  33949  poimirlem4  33950  poimirlem6  33952  poimirlem7  33953  poimirlem9  33955  poimirlem11  33957  poimirlem12  33958  poimirlem16  33962  poimirlem17  33963  poimirlem19  33965  poimirlem20  33966  poimirlem22  33968  poimirlem26  33972  poimirlem27  33973  poimirlem28  33974  poimirlem32  33978  mblfinlem2  33984  dvasin  34032  f1ocan1fv  34057  metf1o  34086  ismtyval  34134  isismty  34135  ismtyima  34137  ismtyhmeolem  34138  ismtybndlem  34140  ismrer1  34172  reheibor  34173  grposnOLD  34216  rngoisocnv  34315  lflnegl  35144  lautset  36150  islaut  36151  lautcl  36155  lautco  36165  pautsetN  36166  ispautN  36167  ldilco  36184  ltrncoidN  36196  ltrncoval  36213  trlcoabs2N  36790  trlcoat  36791  trlcone  36796  cdlemg47a  36802  cdlemg46  36803  cdlemg47  36804  trljco  36808  tgrpgrplem  36817  tendoidcl  36837  tendo0co2  36856  tendo0pl  36859  cdlemi2  36887  cdlemk2  36900  cdlemk4  36902  cdlemk8  36906  cdlemkid2  36992  cdlemk45  37015  cdlemk53b  37024  cdlemk53  37025  cdlemk55a  37027  erng1r  37063  tendocnv  37089  dvalveclem  37093  dva0g  37095  dvhgrp  37175  dvh0g  37179  dvhopN  37184  cdlemn3  37265  cdlemn8  37272  cdlemn9  37273  dihordlem7b  37283  dihopelvalcpre  37316  dihmeetlem1N  37358  dihglblem5apreN  37359  lcfrlem13  37623  hvmapclN  37832  hvmapcl2  37834  mapfzcons  38116  mzpresrename  38150  diophrw  38159  eldioph2  38162  diophren  38214  kelac1  38469  imasgim  38506  lnrfg  38525  brco2f1o  39163  brco3f1o  39164  clsneikex  39237  clsneinex  39238  clsneiel1  39239  neicvgmex  39248  neicvgel1  39250  dssmapntrcls  39259  stoweidlem27  41031  stoweidlem31  41035  stoweidlem39  41043  fourierdlem20  41131  fourierdlem50  41160  fourierdlem52  41162  fourierdlem54  41164  fourierdlem64  41174  fourierdlem76  41186  fourierdlem102  41212  fourierdlem114  41224  sge0f1o  41383  nnfoctbdjlem  41456  isomenndlem  41531  ovnsubaddlem1  41571  f1oresf1o2  42187  isomushgr  42537  isomuspgr  42545  isomgrtrlem  42549  1hegrlfgr  42553  mgmhmf1o  42627  idmgmhm  42628  funcringcsetcALTV2lem8  42883  funcringcsetclem8ALTV  42906  amgmwlem  43437