Theorem f1of 6768

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 6767	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 6724	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 6482  –1-1→wf1 6483  –1-1-onto→wf1o 6485

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 207  df-an 396  df-f1 6491  df-f1o 6493

This theorem is referenced by:  f1ofn  6769  f1ompt  7050  f1oresrab  7066  fsn  7074  fsnunf  7125  f1ounsn  7212  f1ocnvfv1  7216  f1ocnvfv2  7217  fsnex  7223  f1ocnvdm  7225  fcof1oinvd  7233  fveqf1o  7242  isocnv  7270  isocnv3  7272  isores2  7273  isotr  7276  isofr2  7284  isopolem  7285  isosolem  7287  f1oiso2  7292  weniso  7294  f1ofveu  7346  f1oexrnex  7863  f1oabexg  7878  f1oabexgOLD  7879  wemoiso  7911  mptcnfimad  7924  suppsnop  8114  smoiso  8288  mapsnd  8816  ralxpmap  8826  f1oen2g  8897  en1  8953  enfixsn  9006  mapen  9061  ac6sfi  9175  domunfican  9213  fiint  9218  mapfienlem1  9296  mapfienlem2  9297  mapfienlem3  9298  mapfien  9299  supisoex  9366  supiso  9367  ordiso2  9408  unxpwdom2  9481  cantnfle  9568  cantnfp1lem3  9577  cantnflem1b  9583  cantnflem1d  9585  cantnflem1  9586  cnfcomlem  9596  cnfcom  9597  cnfcom2lem  9598  cnfcom2  9599  cnfcom3lem  9600  cnfcom3  9601  cnfcom3clem  9602  djuin  9818  infxpenlem  9911  infxpenc  9916  infxpenc2lem2  9918  fseqenlem1  9922  acndom  9949  acndom2  9952  infpwfien  9960  iunfictbso  10012  infmap2  10115  ackbij2lem2  10137  infpssrlem3  10203  infpssrlem4  10204  fin23lem30  10240  isf32lem6  10256  isf32lem7  10257  isf32lem8  10258  enfin1ai  10282  axcc3  10336  axcclem  10355  ttukeylem7  10413  fpwwe2lem5  10533  fpwwe2lem6  10534  fpwwe2lem8  10536  canthp1lem2  10551  canthp1  10552  pwfseqlem4a  10559  pwfseqlem5  10561  axdc4uzlem  13892  seqf1olem1  13950  seqf1olem2  13951  seqf1o  13952  hashkf  14241  hasheqf1oi  14260  hasheqf1od  14262  hashcl  14265  hashgadd  14286  hashfacen  14363  hashf1lem1  14364  fz1isolem  14370  seqcoll  14373  seqcoll2  14374  cnrecnv  15074  sumeq2ii  15602  summolem3  15623  summolem2a  15624  fsum  15629  fsumf1o  15632  fsumss  15634  fsumcl2lem  15640  fsumadd  15649  fsummulc2  15693  fsumrelem  15716  ackbijnn  15737  prodeq2ii  15820  prodmolem3  15842  prodmolem2a  15843  fprod  15850  fprodf1o  15855  fprodss  15857  fprodser  15858  fprodcl2lem  15859  fprodmul  15869  fproddiv  15870  fprodn0  15888  fproddvdsd  16248  sadcaddlem  16370  sadadd2lem  16372  sadadd3  16374  sadaddlem  16379  sadasslem  16383  sadeq  16385  phimullem  16692  eulerthlem1  16694  eulerthlem2  16695  unbenlem  16822  vdwlem8  16902  0ram  16934  wunndx  17108  xpsaddlem  17479  xpsvsca  17483  xpsle  17485  idfucl  17790  setccatid  17993  setcinv  17999  catcisolem  18019  estrccatid  18040  funcestrcsetclem7  18054  funcestrcsetclem8  18055  funcsetcestrclem7  18069  funcsetcestrclem8  18070  yonffthlem  18190  gsumpropd2lem  18589  mgmhmf1o  18610  idmgmhm  18611  idmhm  18705  mhmf1o  18706  gsumws1  18748  ielefmnd  18797  idghm  19145  ghmf1o  19162  symgbas  19286  elsymgbas  19288  symgbasf  19290  symgbasfi  19293  symg1bas  19305  symggrp  19314  lactghmga  19319  symgfixf1  19351  f1omvdmvd  19357  f1omvdconj  19360  f1omvdco2  19362  pmtrfconj  19380  symggen  19384  pmtrdifellem1  19390  pmtrdifellem2  19391  psgnunilem1  19407  gsumval3eu  19818  gsumval3lem1  19819  gsumval3  19821  gsumzf1o  19826  gsumconst  19848  gsumsub  19862  gsumcom2  19889  dprdfsub  19937  dprdf1o  19948  dprdsn  19952  ablfaclem2  20002  rngisomfv1  20385  rngisom1  20386  rngisomring1  20388  fidomndrnglem  20689  srngcl  20766  lmhmf1o  20982  gsumfsum  21373  zntoslem  21495  islinds2  21752  lindsmm  21767  psrass1lem  21871  psrnegcl  21893  psrlinv  21894  coe1f2  22123  coe1add  22179  evls1rhmlem  22237  evl1sca  22250  pf1ind  22271  mat1dimelbas  22387  mat1f  22398  mdetleib2  22504  mdetrsca  22519  mdetralt  22524  mdetunilem7  22534  mdetunilem9  22536  ssidcn  23171  hmphdis  23712  indishmph  23714  cmphaushmeo  23716  ordthmeolem  23717  txhmeo  23719  qtopf1  23732  ufldom  23878  symgtgp  24022  tsmsf1o  24061  iducn  24198  imasdsf1olem  24289  xpsdsval  24297  imasf1obl  24404  icchmeo  24866  icchmeoOLD  24867  iccpnfcnv  24870  xrhmeo  24872  cnheiborlem  24881  ovolctb  25419  ovoliunlem1  25431  ovoliunlem2  25432  iunmbl2  25486  dyadmbl  25529  vitalilem2  25538  vitalilem3  25539  vitalilem4  25540  vitalilem5  25541  mbfid  25564  dvid  25847  dvexp  25885  dvcnvlem  25908  dvcnv  25909  dvcnvrelem2  25951  dvcnvre  25952  efcvx  26387  reefgim  26388  efif1olem4  26482  eff1olem  26485  logrncl  26504  relogcl  26512  dvrelog  26574  relogcn  26575  logcn  26584  logf1o2  26587  dvlog  26588  dvlog2  26590  advlog  26591  advlogexp  26592  logtayl  26597  logccv  26600  dvcxp1  26677  loglesqrt  26699  asinrebnd  26839  dvatan  26873  efrlim  26907  efrlimOLD  26908  amgmlem  26928  lgamcvg2  26993  wilthlem2  27007  wilthlem3  27008  sqff1o  27120  lgsqrlem4  27288  logdivsum  27472  log2sumbnd  27483  isismt  28513  motcl  28518  motco  28519  cnvmot  28520  motgrp  28522  motcgrg  28523  f1otrg  28850  f1otrge  28851  axlowdimlem10  28931  axcontlem5  28948  axcontlem10  28953  uspgriedgedg  29156  upgrres1  29293  umgrres1  29294  upgriseupth  30189  pliguhgr  30468  dmadjrn  31877  unopnorm  31899  unopadj  31901  unoplin  31902  counop  31903  idcnop  31963  idhmop  31964  unopbd  31997  bracnln  32091  cnvbraval  32092  leopnmid  32120  nmopleid  32121  hmopidmch  32135  hmopidmpj  32136  disjrdx  32573  fmptco1f1o  32617  isoun  32687  padct  32705  fcobij  32707  fcobijfs  32708  fcobijfs2  32709  wrdpmcl  32926  ccatws1f1o  32939  ccatws1f1olast  32940  mndlactf1o  33018  mndractf1o  33019  abliso  33024  symgfcoeu  33058  symgcom  33059  pmtrcnel  33065  pmtrcnel2  33066  pmtrcnelor  33067  wrdpmtrlast  33069  cycpmco2f1  33100  cycpmco2rn  33101  cycpmco2lem2  33103  cycpmco2lem3  33104  cycpmco2lem4  33105  cycpmco2lem5  33106  cycpmco2lem6  33107  cycpmco2lem7  33108  cycpmco2  33109  cycpmconjv  33118  cycpmconjslem1  33130  cycpmconjslem2  33131  cycpmconjs  33132  islinds5  33339  ellspds  33340  1arithidomlem1  33507  1arithidomlem2  33508  1arithidom  33509  mplvrpmlem  33591  mplvrpmfgalem  33592  mplvrpmmhm  33594  mplvrpmrhm  33595  esplylem  33606  esplympl  33607  esplymhp  33608  esplyfv1  33609  esplyfv  33610  esplysply  33611  esplyfval3  33612  tpr2rico  33946  xrge0iifmhm  33973  xrge0pluscn  33974  rrhre  34055  esumf1o  34084  volmeas  34265  eulerpartgbij  34406  eulerpartlemmf  34409  eulerpartlemgvv  34410  eulerpartlemgf  34413  eulerpartlemgs2  34414  eulerpartlemn  34415  ballotlemsima  34550  reprpmtf1o  34660  logdivsqrle  34684  hgt750lemg  34688  vonf1owev  35173  deranglem  35231  derangsn  35235  derangenlem  35236  subfacp1lem4  35248  subfacp1lem5  35249  subfacp1lem6  35250  cvmfolem  35344  cvmliftlem6  35355  poimirlem1  37681  poimirlem2  37682  poimirlem3  37683  poimirlem4  37684  poimirlem6  37686  poimirlem7  37687  poimirlem9  37689  poimirlem11  37691  poimirlem12  37692  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem26  37706  poimirlem27  37707  poimirlem28  37708  poimirlem32  37712  mblfinlem2  37718  dvasin  37764  f1ocan1fv  37786  metf1o  37815  ismtyval  37860  isismty  37861  ismtyima  37863  ismtyhmeolem  37864  ismtybndlem  37866  ismrer1  37898  reheibor  37899  grposnOLD  37942  rngoisocnv  38041  lflnegl  39195  lautset  40201  islaut  40202  lautcl  40206  lautco  40216  pautsetN  40217  ispautN  40218  ldilco  40235  ltrncoidN  40247  ltrncoval  40264  trlcoabs2N  40841  trlcoat  40842  trlcone  40847  cdlemg47a  40853  cdlemg46  40854  cdlemg47  40855  trljco  40859  tgrpgrplem  40868  tendoidcl  40888  tendo0co2  40907  tendo0pl  40910  cdlemi2  40938  cdlemk2  40951  cdlemk4  40953  cdlemk8  40957  cdlemkid2  41043  cdlemk45  41066  cdlemk53b  41075  cdlemk53  41076  cdlemk55a  41078  erng1r  41114  tendocnv  41140  dvalveclem  41144  dva0g  41146  dvhgrp  41226  dvh0g  41230  dvhopN  41235  cdlemn3  41316  cdlemn8  41323  cdlemn9  41324  dihordlem7b  41334  dihopelvalcpre  41367  dihmeetlem1N  41409  dihglblem5apreN  41410  lcfrlem13  41674  hvmapclN  41883  hvmapcl2  41885  dvrelog2  42177  dvrelog3  42178  sticksstones3  42261  sticksstones17  42276  sticksstones18  42277  sticksstones19  42278  readvrec2  42479  readvrec  42480  mapfzcons  42833  mzpresrename  42867  diophrw  42876  eldioph2  42879  diophren  42930  kelac1  43180  imasgim  43217  lnrfg  43236  nvocnvb  43539  brco2f1o  44149  brco3f1o  44150  clsneikex  44223  clsneinex  44224  clsneiel1  44225  neicvgmex  44234  neicvgel1  44236  dssmapntrcls  44245  stoweidlem27  46149  stoweidlem31  46153  stoweidlem39  46161  fourierdlem20  46249  fourierdlem50  46278  fourierdlem52  46280  fourierdlem54  46282  fourierdlem64  46292  fourierdlem76  46304  fourierdlem102  46330  fourierdlem114  46342  sge0f1o  46504  nnfoctbdjlem  46577  isomenndlem  46652  ovnsubaddlem1  46692  3f1oss1  47199  reuf1odnf  47231  reuf1od  47232  f1oresf1o2  47415  fundcmpsurbijinjpreimafv  47531  fundcmpsurinjimaid  47535  grimfn  48003  isgrim  48006  grimuhgr  48011  grimco  48013  uhgrimedgi  48014  isuspgrim0lem  48017  isuspgrim0  48018  isuspgrim  48020  upgrimwlklem4  48024  gricushgr  48041  isubgrgrim  48053  uhgrimisgrgriclem  48054  uhgrimisgrgric  48055  clnbgrgrim  48058  grimedg  48059  grtriclwlk3  48069  isubgr3stgrlem3  48092  isubgr3stgrlem4  48093  isubgr3stgrlem6  48095  isubgr3stgrlem7  48096  isubgr3stgrlem8  48097  isubgr3stgrlem9  48098  grlimfn  48103  isgrlim  48106  uspgrlimlem1  48112  uspgrlimlem2  48113  uspgrlimlem3  48114  uspgrlimlem4  48115  grlimprclnbgredg  48121  grlimgredgex  48124  grlimgrtrilem2  48126  grlictr  48139  clnbgr3stgrgrlim  48143  clnbgr3stgrgrlic  48144  1hegrlfgr  48256  funcringcsetcALTV2lem8  48421  funcringcsetclem8ALTV  48444  itcovalendof  48794  uptrlem1  49335  uptr2  49346  swapf2f1oaALT  49403  swapfcoa  49406  swapffunc  49407  fucoppc  49535  thincciso  49578  thinccisod  49579  lmdran  49796  cmdlan  49797  amgmwlem  49927