Theorem f1of 6803

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

Syntax hints:   → wi 4  ⟶wf 6510  –1-1→wf1 6511  –1-1-onto→wf1o 6513

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 6519  df-f1o 6521

This theorem is referenced by:  f1ofn  6804  f1ompt  7086  f1oresrab  7102  fsn  7110  fsnunf  7162  f1ounsn  7250  f1ocnvfv1  7254  f1ocnvfv2  7255  fsnex  7261  f1ocnvdm  7263  fcof1oinvd  7271  fveqf1o  7280  isocnv  7308  isocnv3  7310  isores2  7311  isotr  7314  isofr2  7322  isopolem  7323  isosolem  7325  f1oiso2  7330  weniso  7332  f1ofveu  7384  f1oexrnex  7906  f1oabexg  7921  f1oabexgOLD  7922  wemoiso  7955  mptcnfimad  7968  suppsnop  8160  smoiso  8334  mapsnd  8862  ralxpmap  8872  f1oen2g  8943  en1  8998  enfixsn  9055  mapen  9111  ac6sfi  9238  domunfican  9279  fiint  9284  fiintOLD  9285  mapfienlem1  9363  mapfienlem2  9364  mapfienlem3  9365  mapfien  9366  supisoex  9433  supiso  9434  ordiso2  9475  unxpwdom2  9548  cantnfle  9631  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1d  9648  cantnflem1  9649  cnfcomlem  9659  cnfcom  9660  cnfcom2lem  9661  cnfcom2  9662  cnfcom3lem  9663  cnfcom3  9664  cnfcom3clem  9665  djuin  9878  infxpenlem  9973  infxpenc  9978  infxpenc2lem2  9980  fseqenlem1  9984  acndom  10011  acndom2  10014  infpwfien  10022  iunfictbso  10074  infmap2  10177  ackbij2lem2  10199  infpssrlem3  10265  infpssrlem4  10266  fin23lem30  10302  isf32lem6  10318  isf32lem7  10319  isf32lem8  10320  enfin1ai  10344  axcc3  10398  axcclem  10417  ttukeylem7  10475  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  canthp1lem2  10613  canthp1  10614  pwfseqlem4a  10621  pwfseqlem5  10623  axdc4uzlem  13955  seqf1olem1  14013  seqf1olem2  14014  seqf1o  14015  hashkf  14304  hasheqf1oi  14323  hasheqf1od  14325  hashcl  14328  hashgadd  14349  hashfacen  14426  hashf1lem1  14427  fz1isolem  14433  seqcoll  14436  seqcoll2  14437  cnrecnv  15138  sumeq2ii  15666  summolem3  15687  summolem2a  15688  fsum  15693  fsumf1o  15696  fsumss  15698  fsumcl2lem  15704  fsumadd  15713  fsummulc2  15757  fsumrelem  15780  ackbijnn  15801  prodeq2ii  15884  prodmolem3  15906  prodmolem2a  15907  fprod  15914  fprodf1o  15919  fprodss  15921  fprodser  15922  fprodcl2lem  15923  fprodmul  15933  fproddiv  15934  fprodn0  15952  fproddvdsd  16312  sadcaddlem  16434  sadadd2lem  16436  sadadd3  16438  sadaddlem  16443  sadasslem  16447  sadeq  16449  phimullem  16756  eulerthlem1  16758  eulerthlem2  16759  unbenlem  16886  vdwlem8  16966  0ram  16998  wunndx  17172  xpsaddlem  17543  xpsvsca  17547  xpsle  17549  idfucl  17850  setccatid  18053  setcinv  18059  catcisolem  18079  estrccatid  18100  funcestrcsetclem7  18114  funcestrcsetclem8  18115  funcsetcestrclem7  18129  funcsetcestrclem8  18130  yonffthlem  18250  gsumpropd2lem  18613  mgmhmf1o  18634  idmgmhm  18635  idmhm  18729  mhmf1o  18730  gsumws1  18772  ielefmnd  18821  idghm  19170  ghmf1o  19187  symgbas  19309  elsymgbas  19311  symgbasf  19313  symgbasfi  19316  symg1bas  19328  symggrp  19337  lactghmga  19342  symgfixf1  19374  f1omvdmvd  19380  f1omvdconj  19383  f1omvdco2  19385  pmtrfconj  19403  symggen  19407  pmtrdifellem1  19413  pmtrdifellem2  19414  psgnunilem1  19430  gsumval3eu  19841  gsumval3lem1  19842  gsumval3  19844  gsumzf1o  19849  gsumconst  19871  gsumsub  19885  gsumcom2  19912  dprdfsub  19960  dprdf1o  19971  dprdsn  19975  ablfaclem2  20025  rngisomfv1  20381  rngisom1  20382  rngisomring1  20384  fidomndrnglem  20688  srngcl  20765  lmhmf1o  20960  gsumfsum  21358  zntoslem  21473  islinds2  21729  lindsmm  21744  psrass1lem  21848  psrnegcl  21870  psrlinv  21871  coe1f2  22101  coe1add  22157  evls1rhmlem  22215  evl1sca  22228  pf1ind  22249  mat1dimelbas  22365  mat1f  22376  mdetleib2  22482  mdetrsca  22497  mdetralt  22502  mdetunilem7  22512  mdetunilem9  22514  ssidcn  23149  hmphdis  23690  indishmph  23692  cmphaushmeo  23694  ordthmeolem  23695  txhmeo  23697  qtopf1  23710  ufldom  23856  symgtgp  24000  tsmsf1o  24039  iducn  24177  imasdsf1olem  24268  xpsdsval  24276  imasf1obl  24383  icchmeo  24845  icchmeoOLD  24846  iccpnfcnv  24849  xrhmeo  24851  cnheiborlem  24860  ovolctb  25398  ovoliunlem1  25410  ovoliunlem2  25411  iunmbl2  25465  dyadmbl  25508  vitalilem2  25517  vitalilem3  25518  vitalilem4  25519  vitalilem5  25520  mbfid  25543  dvid  25826  dvexp  25864  dvcnvlem  25887  dvcnv  25888  dvcnvrelem2  25930  dvcnvre  25931  efcvx  26366  reefgim  26367  efif1olem4  26461  eff1olem  26464  logrncl  26483  relogcl  26491  dvrelog  26553  relogcn  26554  logcn  26563  logf1o2  26566  dvlog  26567  dvlog2  26569  advlog  26570  advlogexp  26571  logtayl  26576  logccv  26579  dvcxp1  26656  loglesqrt  26678  asinrebnd  26818  dvatan  26852  efrlim  26886  efrlimOLD  26887  amgmlem  26907  lgamcvg2  26972  wilthlem2  26986  wilthlem3  26987  sqff1o  27099  lgsqrlem4  27267  logdivsum  27451  log2sumbnd  27462  isismt  28468  motcl  28473  motco  28474  cnvmot  28475  motgrp  28477  motcgrg  28478  f1otrg  28805  f1otrge  28806  axlowdimlem10  28885  axcontlem5  28902  axcontlem10  28907  uspgriedgedg  29110  upgrres1  29247  umgrres1  29248  upgriseupth  30143  pliguhgr  30422  dmadjrn  31831  unopnorm  31853  unopadj  31855  unoplin  31856  counop  31857  idcnop  31917  idhmop  31918  unopbd  31951  bracnln  32045  cnvbraval  32046  leopnmid  32074  nmopleid  32075  hmopidmch  32089  hmopidmpj  32090  disjrdx  32527  fmptco1f1o  32564  isoun  32632  padct  32650  fcobij  32652  fcobijfs  32653  wrdpmcl  32866  ccatws1f1o  32880  ccatws1f1olast  32881  mndlactf1o  32978  mndractf1o  32979  abliso  32984  symgfcoeu  33046  symgcom  33047  pmtrcnel  33053  pmtrcnel2  33054  pmtrcnelor  33055  wrdpmtrlast  33057  cycpmco2f1  33088  cycpmco2rn  33089  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  cycpmconjv  33106  cycpmconjslem1  33118  cycpmconjslem2  33119  cycpmconjs  33120  islinds5  33345  ellspds  33346  1arithidomlem1  33513  1arithidomlem2  33514  1arithidom  33515  tpr2rico  33909  xrge0iifmhm  33936  xrge0pluscn  33937  rrhre  34018  esumf1o  34047  volmeas  34228  eulerpartgbij  34370  eulerpartlemmf  34373  eulerpartlemgvv  34374  eulerpartlemgf  34377  eulerpartlemgs2  34378  eulerpartlemn  34379  ballotlemsima  34514  reprpmtf1o  34624  logdivsqrle  34648  hgt750lemg  34652  vonf1owev  35102  deranglem  35160  derangsn  35164  derangenlem  35165  subfacp1lem4  35177  subfacp1lem5  35178  subfacp1lem6  35179  cvmfolem  35273  cvmliftlem6  35284  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem9  37630  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem32  37653  mblfinlem2  37659  dvasin  37705  f1ocan1fv  37727  metf1o  37756  ismtyval  37801  isismty  37802  ismtyima  37804  ismtyhmeolem  37805  ismtybndlem  37807  ismrer1  37839  reheibor  37840  grposnOLD  37883  rngoisocnv  37982  lflnegl  39076  lautset  40083  islaut  40084  lautcl  40088  lautco  40098  pautsetN  40099  ispautN  40100  ldilco  40117  ltrncoidN  40129  ltrncoval  40146  trlcoabs2N  40723  trlcoat  40724  trlcone  40729  cdlemg47a  40735  cdlemg46  40736  cdlemg47  40737  trljco  40741  tgrpgrplem  40750  tendoidcl  40770  tendo0co2  40789  tendo0pl  40792  cdlemi2  40820  cdlemk2  40833  cdlemk4  40835  cdlemk8  40839  cdlemkid2  40925  cdlemk45  40948  cdlemk53b  40957  cdlemk53  40958  cdlemk55a  40960  erng1r  40996  tendocnv  41022  dvalveclem  41026  dva0g  41028  dvhgrp  41108  dvh0g  41112  dvhopN  41117  cdlemn3  41198  cdlemn8  41205  cdlemn9  41206  dihordlem7b  41216  dihopelvalcpre  41249  dihmeetlem1N  41291  dihglblem5apreN  41292  lcfrlem13  41556  hvmapclN  41765  hvmapcl2  41767  dvrelog2  42059  dvrelog3  42060  sticksstones3  42143  sticksstones17  42158  sticksstones18  42159  sticksstones19  42160  readvrec2  42356  readvrec  42357  mapfzcons  42711  mzpresrename  42745  diophrw  42754  eldioph2  42757  diophren  42808  kelac1  43059  imasgim  43096  lnrfg  43115  nvocnvb  43418  brco2f1o  44028  brco3f1o  44029  clsneikex  44102  clsneinex  44103  clsneiel1  44104  neicvgmex  44113  neicvgel1  44115  dssmapntrcls  44124  stoweidlem27  46032  stoweidlem31  46036  stoweidlem39  46044  fourierdlem20  46132  fourierdlem50  46161  fourierdlem52  46163  fourierdlem54  46165  fourierdlem64  46175  fourierdlem76  46187  fourierdlem102  46213  fourierdlem114  46225  sge0f1o  46387  nnfoctbdjlem  46460  isomenndlem  46535  ovnsubaddlem1  46575  3f1oss1  47080  reuf1odnf  47112  reuf1od  47113  f1oresf1o2  47296  fundcmpsurbijinjpreimafv  47412  fundcmpsurinjimaid  47416  grimfn  47883  isgrim  47886  grimuhgr  47891  grimco  47893  uhgrimedgi  47894  isuspgrim0lem  47897  isuspgrim0  47898  isuspgrim  47900  upgrimwlklem4  47904  gricushgr  47921  isubgrgrim  47933  uhgrimisgrgriclem  47934  uhgrimisgrgric  47935  clnbgrgrim  47938  grimedg  47939  grtriclwlk3  47948  isubgr3stgrlem3  47971  isubgr3stgrlem4  47972  isubgr3stgrlem6  47974  isubgr3stgrlem7  47975  isubgr3stgrlem8  47976  isubgr3stgrlem9  47977  grlimfn  47982  isgrlim  47985  uspgrlimlem1  47991  uspgrlimlem2  47992  uspgrlimlem3  47993  uspgrlimlem4  47994  grlimgrtrilem2  47998  grlictr  48011  clnbgr3stgrgrlic  48015  1hegrlfgr  48124  funcringcsetcALTV2lem8  48289  funcringcsetclem8ALTV  48312  itcovalendof  48662  uptrlem1  49203  uptr2  49214  swapf2f1oaALT  49271  swapfcoa  49274  swapffunc  49275  fucoppc  49403  thincciso  49446  thinccisod  49447  lmdran  49664  cmdlan  49665  amgmwlem  49795