Theorem f1of 6824

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

This proof depends on syntax axioms:   → wi 4  ⟶wf 6534  –1-1→wf1 6535  –1-1-onto→wf1o 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f1 6543  df-f1o 6545

This theorem is used by:  f1ofn  6825  f1ompt  7111  f1oresrab  7128  fsn  7136  fsnunf  7190  f1ounsn  7280  f1ocnvfv1  7284  f1ocnvfv2  7285  fsnex  7291  f1ocnvdm  7293  fcof1oinvd  7301  fveqf1o  7310  isocnv  7338  isocnv3  7340  isores2  7341  isotr  7344  isofr2  7352  isopolem  7353  isosolem  7355  f1oiso2  7360  weniso  7364  f1ofveu  7414  f1oexrnex  7939  f1oabexg  7953  wemoiso  7985  mptcnfimad  7998  suppsnop  8198  smoiso  8373  mapsnd  8917  ralxpmap  8927  f1oen2g  8998  en1  9054  enfixsn  9108  mapen  9163  ac6sfi  9278  domunfican  9316  fiint  9321  mapfienlem1  9400  mapfienlem2  9401  mapfienlem3  9402  mapfien  9403  supisoex  9470  supiso  9471  ordiso2  9512  unxpwdom2  9585  cantnfle  9675  cantnfp1lem3  9684  cantnflem1b  9690  cantnflem1d  9692  cantnflem1  9693  cnfcomlem  9703  cnfcom  9704  cnfcom2lem  9705  cnfcom2  9706  cnfcom3lem  9707  cnfcom3  9708  cnfcom3clem  9709  djuin  10002  infxpenlem  10095  infxpenc  10100  infxpenc2lem2  10102  fseqenlem1  10106  acndom  10133  acndom2  10136  infpwfien  10144  iunfictbso  10196  infmap2  10298  ackbij2lem2  10320  infpssrlem3  10386  infpssrlem4  10387  fin23lem30  10423  isf32lem6  10439  isf32lem7  10440  isf32lem8  10441  enfin1ai  10465  axcc3  10519  axcclem  10538  ttukeylem7  10596  fpwwe2lem5  10723  fpwwe2lem6  10724  fpwwe2lem8  10726  canthp1lem2  10741  canthp1  10742  pwfseqlem4a  10749  pwfseqlem5  10751  axdc4uzlem  14129  seqf1olem1  14187  seqf1olem2  14188  seqf1o  14189  hashkf  14479  hasheqf1oi  14498  hasheqf1od  14500  hashcl  14503  hashgadd  14524  hashfacen  14602  hashf1lem1  14603  fz1isolem  14609  seqcoll  14612  seqcoll2  14613  cnrecnv  15337  sumeq2ii  15865  summolem3  15885  summolem2a  15886  fsum  15891  fsumf1o  15894  fsumss  15896  fsumcl2lem  15902  fsumadd  15911  fsummulc2  15955  fsumrelem  15979  ackbijnn  16002  prodeq2ii  16085  prodmolem3  16105  prodmolem2a  16106  fprod  16113  fprodf1o  16118  fprodss  16120  fprodser  16121  fprodcl2lem  16122  fprodmul  16132  fproddiv  16133  fprodn0  16151  fproddvdsd  16510  sadcaddlem  16632  sadadd2lem  16634  sadadd3  16636  sadaddlem  16641  sadasslem  16645  sadeq  16647  phimullem  16961  eulerthlem1  16963  eulerthlem2  16964  unbenlem  17091  vdwlem8  17171  0ram  17203  wunndx  17378  xpsaddlem  17750  xpsvsca  17754  xpsle  17756  idfucl  18061  setccatid  18264  setcinv  18270  catcisolem  18290  estrccatid  18311  funcestrcsetclem7  18325  funcestrcsetclem8  18326  funcsetcestrclem7  18340  funcsetcestrclem8  18341  yonffthlem  18461  gsumpropd2lem  18873  mgmhmf1o  18894  idmgmhm  18895  idmhm  18995  mhmf1o  18996  gsumws1  19039  ielefmnd  19088  idghm  19450  ghmf1o  19467  symgbas  19591  elsymgbas  19593  symgbasf  19595  symgbasfi  19598  symg1bas  19610  symggrp  19619  lactghmga  19624  symgfixf1  19656  f1omvdmvd  19662  f1omvdconj  19665  f1omvdco2  19667  pmtrfconj  19685  symggen  19689  pmtrdifellem1  19695  pmtrdifellem2  19696  psgnunilem1  19712  gsumval3eu  20123  gsumval3lem1  20124  gsumval3  20126  gsumzf1o  20131  gsumconst  20153  gsumsub  20167  gsumcom2  20194  dprdfsub  20242  dprdf1o  20253  dprdsn  20257  ablfaclem2  20307  rngisomfv1  20700  rngisom1  20701  rngisomring1  20703  fidomndrnglem  21035  srngcl  21111  lmhmf1o  21326  gsumfsum  21745  zntoslem  21867  islinds2  22124  lindsmm  22139  psrass1lem  22246  psrnegcl  22267  psrlinv  22268  coe1f2  22532  coe1add  22588  evls1rhmlem  22644  evl1sca  22657  pf1ind  22678  mat1dimelbas  22791  mat1f  22802  mdetleib2  22908  mdetrsca  22923  mdetralt  22928  mdetunilem7  22938  mdetunilem9  22940  ssidcn  23578  hmphdis  24120  indishmph  24122  cmphaushmeo  24124  ordthmeolem  24125  txhmeo  24127  qtopf1  24140  ufldom  24286  symgtgp  24430  tsmsf1o  24469  iducn  24606  imasdsf1olem  24697  xpsdsval  24705  imasf1obl  24812  icchmeo  25267  iccpnfcnv  25270  xrhmeo  25272  cnheiborlem  25280  ovolctb  25816  ovoliunlem1  25828  ovoliunlem2  25829  iunmbl2  25883  dyadmbl  25926  vitalilem2  25935  vitalilem3  25936  vitalilem4  25937  vitalilem5  25938  mbfid  25961  dvid  26243  dvexp  26278  dvcnvlem  26301  dvcnv  26302  dvcnvrelem2  26343  dvcnvre  26344  efcvx  26781  reefgim  26782  efif1olem4  26878  eff1olem  26881  logrncl  26900  relogcl  26908  dvrelog  26970  relogcn  26971  logcn  26980  logf1o2  26983  dvlog  26984  dvlog2  26986  advlog  26987  advlogexp  26988  logtayl  26993  logccv  26996  dvcxp1  27073  loglesqrt  27094  asinrebnd  27234  dvatan  27268  efrlim  27302  amgmlem  27322  lgamcvg2  27387  wilthlem2  27401  wilthlem3  27402  sqff1o  27514  lgsqrlem4  27681  logdivsum  27865  log2sumbnd  27876  isismt  29002  motcl  29007  motco  29008  cnvmot  29009  motgrp  29011  motcgrg  29012  f1otrg  29453  f1otrge  29454  axlowdimlem10  29534  axcontlem5  29551  axcontlem10  29556  uspgriedgedg  29762  upgrres1  29899  umgrres1  29900  upgriseupth  30813  pliguhgr  31093  dmadjrn  32502  unopnorm  32524  unopadj  32526  unoplin  32527  counop  32528  idcnop  32588  idhmop  32589  unopbd  32622  bracnln  32716  cnvbraval  32717  leopnmid  32745  nmopleid  32746  hmopidmch  32760  hmopidmpj  32761  disjrdx  33232  fmptco1f1o  33274  isoun  33342  padct  33357  fcobij  33358  fcobijfs  33359  fcobijfs2  33360  wrdpmcl  33551  ccatws1f1o  33560  ccatws1f1olast  33561  mndlactf1o  33637  mndractf1o  33638  abliso  33642  symgfcoeu  33689  symgcom  33690  pmtrcnel  33696  pmtrcnel2  33697  pmtrcnelor  33698  wrdpmtrlast  33700  cycpmco2f1  33731  cycpmco2rn  33732  cycpmco2lem2  33734  cycpmco2lem3  33735  cycpmco2lem4  33736  cycpmco2lem5  33737  cycpmco2lem6  33738  cycpmco2lem7  33739  cycpmco2  33740  cycpmconjv  33749  cycpmconjslem1  33761  cycpmconjslem2  33762  cycpmconjs  33763  islinds5  33969  ellspds  33970  1arithidomlem1  34113  1arithidomlem2  34114  1arithidom  34115  0mplrim  34192  selvply1rhmlemb  34197  mplvrpmlem  34221  mplvrpmfgalem  34222  mplvrpmmhm  34224  mplvrpmrhm  34225  esplyfval0  34242  esplylem  34244  esplympl  34245  esplymhp  34246  esplyfv1  34247  esplyfv  34248  esplysply  34249  esplyfval3  34250  vieta  34258  tpr2rico  34590  xrge0iifmhm  34617  xrge0pluscn  34618  rrhre  34699  esumf1o  34728  volmeas  34910  eulerpartgbij  35050  eulerpartlemmf  35053  eulerpartlemgvv  35054  eulerpartlemgf  35057  eulerpartlemgs2  35058  eulerpartlemn  35059  ballotlemsima  35194  reprpmtf1o  35301  logdivsqrle  35325  hgt750lemg  35329  j00smo  35944  maxssj0  35945  j0ltalephlem  35946  j0ltaleph  35947  vonf1owevOLD  35957  deranglem  36017  derangsn  36021  derangenlem  36022  subfacp1lem4  36034  subfacp1lem5  36035  subfacp1lem6  36036  cvmfolem  36130  cvmliftlem6  36141  poimirlem1  38632  poimirlem2  38633  poimirlem3  38634  poimirlem4  38635  poimirlem6  38637  poimirlem7  38638  poimirlem9  38640  poimirlem11  38642  poimirlem12  38643  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem20  38651  poimirlem22  38653  poimirlem26  38657  poimirlem27  38658  poimirlem28  38659  poimirlem32  38663  mblfinlem2  38669  dvasin  38715  f1ocan1fv  38753  metf1o  38782  ismtyval  38827  isismty  38828  ismtyima  38830  ismtyhmeolem  38831  ismtybndlem  38833  ismrer1  38865  reheibor  38866  grposnOLD  38909  rngoisocnv  39008  lflnegl  40226  lautset  41232  islaut  41233  lautcl  41237  lautco  41247  pautsetN  41248  ispautN  41249  ldilco  41266  ltrncoidN  41278  ltrncoval  41295  trlcoabs2N  41872  trlcoat  41873  trlcone  41878  cdlemg47a  41884  cdlemg46  41885  cdlemg47  41886  trljco  41890  tgrpgrplem  41899  tendoidcl  41919  tendo0co2  41938  tendo0pl  41941  cdlemi2  41969  cdlemk2  41982  cdlemk4  41984  cdlemk8  41988  cdlemkid2  42074  cdlemk45  42097  cdlemk53b  42106  cdlemk53  42107  cdlemk55a  42109  erng1r  42145  tendocnv  42171  dvalveclem  42175  dva0g  42177  dvhgrp  42257  dvh0g  42261  dvhopN  42266  cdlemn3  42347  cdlemn8  42354  cdlemn9  42355  dihordlem7b  42365  dihopelvalcpre  42398  dihmeetlem1N  42440  dihglblem5apreN  42441  lcfrlem13  42705  hvmapclN  42914  hvmapcl2  42916  dvrelog2  43207  dvrelog3  43208  sticksstones3  43291  sticksstones17  43306  sticksstones18  43307  sticksstones19  43308  readvrec2  43505  readvrec  43506  mapfzcons  43820  mzpresrename  43854  diophrw  43863  eldioph2  43866  diophren  43913  kelac1  44158  imasgim  44195  lnrfg  44214  nvocnvb  44516  brco2f1o  45125  brco3f1o  45126  clsneikex  45199  clsneinex  45200  clsneiel1  45201  neicvgmex  45210  neicvgel1  45212  dssmapntrcls  45221  stoweidlem27  47130  stoweidlem31  47134  stoweidlem39  47142  fourierdlem20  47230  fourierdlem50  47259  fourierdlem52  47261  fourierdlem54  47263  fourierdlem64  47273  fourierdlem76  47285  fourierdlem102  47311  fourierdlem114  47323  sge0f1o  47485  nnfoctbdjlem  47558  isomenndlem  47633  ovnsubaddlem1  47673  3f1oss1  48238  reuf1odnf  48270  reuf1od  48271  f1oresf1o2  48454  fundcmpsurbijinjpreimafv  48582  fundcmpsurinjimaid  48586  grimfn  49070  isgrim  49073  grimuhgr  49078  grimco  49080  uhgrimedgi  49081  isuspgrim0lem  49084  isuspgrim0  49085  isuspgrim  49087  upgrimwlklem4  49091  gricushgr  49108  isubgrgrim  49120  uhgrimisgrgriclem  49121  uhgrimisgrgric  49122  clnbgrgrim  49125  grimedg  49126  grtriclwlk3  49136  isubgr3stgrlem3  49159  isubgr3stgrlem4  49160  isubgr3stgrlem6  49162  isubgr3stgrlem7  49163  isubgr3stgrlem8  49164  isubgr3stgrlem9  49165  grlimfn  49170  isgrlim  49173  uspgrlimlem1  49179  uspgrlimlem2  49180  uspgrlimlem3  49181  uspgrlimlem4  49182  grlimprclnbgredg  49188  grlimgredgex  49191  grlimgrtrilem2  49193  grlictr  49206  clnbgr3stgrgrlim  49210  clnbgr3stgrgrlic  49211  1hegrlfgr  49323  funcringcsetcALTV2lem8  49487  funcringcsetclem8ALTV  49510  itcovalendof  49874  uptrlem1  50419  uptr2  50430  swapf2f1oaALT  50493  swapfcoa  50496  swapffunc  50497  fucoppc  50638  thincciso  50681  thinccisod  50682  parmapfunc2  50867  parmapfunc  50868  lmdran  50947  cmdlan  50948  amgmwlem  51155