Theorem f1of 6816

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

This proof depends on syntax axioms:   → wi 4  ⟶wf 6527  –1-1→wf1 6528  –1-1-onto→wf1o 6530

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 6536  df-f1o 6538

This theorem is used by:  f1ofn  6817  f1ompt  7103  f1oresrab  7120  fsn  7128  fsnunf  7182  f1ounsn  7272  f1ocnvfv1  7276  f1ocnvfv2  7277  fsnex  7283  f1ocnvdm  7285  fcof1oinvd  7293  fveqf1o  7302  isocnv  7330  isocnv3  7332  isores2  7333  isotr  7336  isofr2  7344  isopolem  7345  isosolem  7347  f1oiso2  7352  weniso  7356  f1ofveu  7406  f1oexrnex  7928  f1oabexg  7942  wemoiso  7974  mptcnfimad  7987  suppsnop  8179  smoiso  8354  mapsnd  8898  ralxpmap  8908  f1oen2g  8979  en1  9035  enfixsn  9089  mapen  9144  ac6sfi  9259  domunfican  9297  fiint  9302  mapfienlem1  9381  mapfienlem2  9382  mapfienlem3  9383  mapfien  9384  supisoex  9451  supiso  9452  ordiso2  9493  unxpwdom2  9566  cantnfle  9656  cantnfp1lem3  9665  cantnflem1b  9671  cantnflem1d  9673  cantnflem1  9674  cnfcomlem  9684  cnfcom  9685  cnfcom2lem  9686  cnfcom2  9687  cnfcom3lem  9688  cnfcom3  9689  cnfcom3clem  9690  djuin  9980  infxpenlem  10073  infxpenc  10078  infxpenc2lem2  10080  fseqenlem1  10084  acndom  10111  acndom2  10114  infpwfien  10122  iunfictbso  10174  infmap2  10276  ackbij2lem2  10298  infpssrlem3  10364  infpssrlem4  10365  fin23lem30  10401  isf32lem6  10417  isf32lem7  10418  isf32lem8  10419  enfin1ai  10443  axcc3  10497  axcclem  10516  ttukeylem7  10574  fpwwe2lem5  10701  fpwwe2lem6  10702  fpwwe2lem8  10704  canthp1lem2  10719  canthp1  10720  pwfseqlem4a  10727  pwfseqlem5  10729  axdc4uzlem  14106  seqf1olem1  14164  seqf1olem2  14165  seqf1o  14166  hashkf  14456  hasheqf1oi  14475  hasheqf1od  14477  hashcl  14480  hashgadd  14501  hashfacen  14579  hashf1lem1  14580  fz1isolem  14586  seqcoll  14589  seqcoll2  14590  cnrecnv  15312  sumeq2ii  15840  summolem3  15860  summolem2a  15861  fsum  15866  fsumf1o  15869  fsumss  15871  fsumcl2lem  15877  fsumadd  15886  fsummulc2  15930  fsumrelem  15954  ackbijnn  15977  prodeq2ii  16060  prodmolem3  16080  prodmolem2a  16081  fprod  16088  fprodf1o  16093  fprodss  16095  fprodser  16096  fprodcl2lem  16097  fprodmul  16107  fproddiv  16108  fprodn0  16126  fproddvdsd  16485  sadcaddlem  16607  sadadd2lem  16609  sadadd3  16611  sadaddlem  16616  sadasslem  16620  sadeq  16622  phimullem  16936  eulerthlem1  16938  eulerthlem2  16939  unbenlem  17066  vdwlem8  17146  0ram  17178  wunndx  17353  xpsaddlem  17725  xpsvsca  17729  xpsle  17731  idfucl  18036  setccatid  18239  setcinv  18245  catcisolem  18265  estrccatid  18286  funcestrcsetclem7  18300  funcestrcsetclem8  18301  funcsetcestrclem7  18315  funcsetcestrclem8  18316  yonffthlem  18436  gsumpropd2lem  18848  mgmhmf1o  18869  idmgmhm  18870  idmhm  18970  mhmf1o  18971  gsumws1  19014  ielefmnd  19063  idghm  19425  ghmf1o  19442  symgbas  19566  elsymgbas  19568  symgbasf  19570  symgbasfi  19573  symg1bas  19585  symggrp  19594  lactghmga  19599  symgfixf1  19631  f1omvdmvd  19637  f1omvdconj  19640  f1omvdco2  19642  pmtrfconj  19660  symggen  19664  pmtrdifellem1  19670  pmtrdifellem2  19671  psgnunilem1  19687  gsumval3eu  20098  gsumval3lem1  20099  gsumval3  20101  gsumzf1o  20106  gsumconst  20128  gsumsub  20142  gsumcom2  20169  dprdfsub  20217  dprdf1o  20228  dprdsn  20232  ablfaclem2  20282  rngisomfv1  20675  rngisom1  20676  rngisomring1  20678  fidomndrnglem  21010  srngcl  21086  lmhmf1o  21301  gsumfsum  21720  zntoslem  21842  islinds2  22099  lindsmm  22114  psrass1lem  22221  psrnegcl  22242  psrlinv  22243  coe1f2  22507  coe1add  22563  evls1rhmlem  22619  evl1sca  22632  pf1ind  22653  mat1dimelbas  22766  mat1f  22777  mdetleib2  22883  mdetrsca  22898  mdetralt  22903  mdetunilem7  22913  mdetunilem9  22915  ssidcn  23553  hmphdis  24095  indishmph  24097  cmphaushmeo  24099  ordthmeolem  24100  txhmeo  24102  qtopf1  24115  ufldom  24261  symgtgp  24405  tsmsf1o  24444  iducn  24581  imasdsf1olem  24672  xpsdsval  24680  imasf1obl  24787  icchmeo  25242  iccpnfcnv  25245  xrhmeo  25247  cnheiborlem  25255  ovolctb  25791  ovoliunlem1  25803  ovoliunlem2  25804  iunmbl2  25858  dyadmbl  25901  vitalilem2  25910  vitalilem3  25911  vitalilem4  25912  vitalilem5  25913  mbfid  25936  dvid  26218  dvexp  26253  dvcnvlem  26276  dvcnv  26277  dvcnvrelem2  26318  dvcnvre  26319  efcvx  26758  reefgim  26759  efif1olem4  26855  eff1olem  26858  logrncl  26877  relogcl  26885  dvrelog  26947  relogcn  26948  logcn  26957  logf1o2  26960  dvlog  26961  dvlog2  26963  advlog  26964  advlogexp  26965  logtayl  26970  logccv  26973  dvcxp1  27050  loglesqrt  27071  asinrebnd  27211  dvatan  27245  efrlim  27279  amgmlem  27299  lgamcvg2  27364  wilthlem2  27378  wilthlem3  27379  sqff1o  27491  lgsqrlem4  27658  logdivsum  27842  log2sumbnd  27853  isismt  28979  motcl  28984  motco  28985  cnvmot  28986  motgrp  28988  motcgrg  28989  f1otrg  29430  f1otrge  29431  axlowdimlem10  29511  axcontlem5  29528  axcontlem10  29533  uspgriedgedg  29739  upgrres1  29876  umgrres1  29877  upgriseupth  30790  pliguhgr  31070  dmadjrn  32479  unopnorm  32501  unopadj  32503  unoplin  32504  counop  32505  idcnop  32565  idhmop  32566  unopbd  32599  bracnln  32693  cnvbraval  32694  leopnmid  32722  nmopleid  32723  hmopidmch  32737  hmopidmpj  32738  disjrdx  33167  fmptco1f1o  33209  isoun  33277  padct  33292  fcobij  33294  fcobijfs  33295  fcobijfs2  33296  wrdpmcl  33487  ccatws1f1o  33496  ccatws1f1olast  33497  mndlactf1o  33573  mndractf1o  33574  abliso  33578  symgfcoeu  33625  symgcom  33626  pmtrcnel  33632  pmtrcnel2  33633  pmtrcnelor  33634  wrdpmtrlast  33636  cycpmco2f1  33667  cycpmco2rn  33668  cycpmco2lem2  33670  cycpmco2lem3  33671  cycpmco2lem4  33672  cycpmco2lem5  33673  cycpmco2lem6  33674  cycpmco2lem7  33675  cycpmco2  33676  cycpmconjv  33685  cycpmconjslem1  33697  cycpmconjslem2  33698  cycpmconjs  33699  islinds5  33905  ellspds  33906  1arithidomlem1  34049  1arithidomlem2  34050  1arithidom  34051  0mplrim  34128  selvply1rhmlemb  34133  mplvrpmlem  34157  mplvrpmfgalem  34158  mplvrpmmhm  34160  mplvrpmrhm  34161  esplyfval0  34178  esplylem  34180  esplympl  34181  esplymhp  34182  esplyfv1  34183  esplyfv  34184  esplysply  34185  esplyfval3  34186  vieta  34194  tpr2rico  34526  xrge0iifmhm  34553  xrge0pluscn  34554  rrhre  34635  esumf1o  34664  volmeas  34846  eulerpartgbij  34987  eulerpartlemmf  34990  eulerpartlemgvv  34991  eulerpartlemgf  34994  eulerpartlemgs2  34995  eulerpartlemn  34996  ballotlemsima  35131  reprpmtf1o  35238  logdivsqrle  35262  hgt750lemg  35266  vonf1owevOLD  35862  deranglem  35900  derangsn  35904  derangenlem  35905  subfacp1lem4  35917  subfacp1lem5  35918  subfacp1lem6  35919  cvmfolem  36013  cvmliftlem6  36024  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem9  38515  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem22  38528  poimirlem26  38532  poimirlem27  38533  poimirlem28  38534  poimirlem32  38538  mblfinlem2  38544  dvasin  38590  f1ocan1fv  38628  metf1o  38657  ismtyval  38702  isismty  38703  ismtyima  38705  ismtyhmeolem  38706  ismtybndlem  38708  ismrer1  38740  reheibor  38741  grposnOLD  38784  rngoisocnv  38883  lflnegl  40101  lautset  41107  islaut  41108  lautcl  41112  lautco  41122  pautsetN  41123  ispautN  41124  ldilco  41141  ltrncoidN  41153  ltrncoval  41170  trlcoabs2N  41747  trlcoat  41748  trlcone  41753  cdlemg47a  41759  cdlemg46  41760  cdlemg47  41761  trljco  41765  tgrpgrplem  41774  tendoidcl  41794  tendo0co2  41813  tendo0pl  41816  cdlemi2  41844  cdlemk2  41857  cdlemk4  41859  cdlemk8  41863  cdlemkid2  41949  cdlemk45  41972  cdlemk53b  41981  cdlemk53  41982  cdlemk55a  41984  erng1r  42020  tendocnv  42046  dvalveclem  42050  dva0g  42052  dvhgrp  42132  dvh0g  42136  dvhopN  42141  cdlemn3  42222  cdlemn8  42229  cdlemn9  42230  dihordlem7b  42240  dihopelvalcpre  42273  dihmeetlem1N  42315  dihglblem5apreN  42316  lcfrlem13  42580  hvmapclN  42789  hvmapcl2  42791  dvrelog2  43082  dvrelog3  43083  sticksstones3  43166  sticksstones17  43181  sticksstones18  43182  sticksstones19  43183  readvrec2  43380  readvrec  43381  mapfzcons  43680  mzpresrename  43714  diophrw  43723  eldioph2  43726  diophren  43773  kelac1  44023  imasgim  44060  lnrfg  44079  nvocnvb  44381  brco2f1o  44991  brco3f1o  44992  clsneikex  45065  clsneinex  45066  clsneiel1  45067  neicvgmex  45076  neicvgel1  45078  dssmapntrcls  45087  stoweidlem27  46981  stoweidlem31  46985  stoweidlem39  46993  fourierdlem20  47081  fourierdlem50  47110  fourierdlem52  47112  fourierdlem54  47114  fourierdlem64  47124  fourierdlem76  47136  fourierdlem102  47162  fourierdlem114  47174  sge0f1o  47336  nnfoctbdjlem  47409  isomenndlem  47484  ovnsubaddlem1  47524  3f1oss1  48089  reuf1odnf  48121  reuf1od  48122  f1oresf1o2  48305  fundcmpsurbijinjpreimafv  48433  fundcmpsurinjimaid  48437  grimfn  48921  isgrim  48924  grimuhgr  48929  grimco  48931  uhgrimedgi  48932  isuspgrim0lem  48935  isuspgrim0  48936  isuspgrim  48938  upgrimwlklem4  48942  gricushgr  48959  isubgrgrim  48971  uhgrimisgrgriclem  48972  uhgrimisgrgric  48973  clnbgrgrim  48976  grimedg  48977  grtriclwlk3  48987  isubgr3stgrlem3  49010  isubgr3stgrlem4  49011  isubgr3stgrlem6  49013  isubgr3stgrlem7  49014  isubgr3stgrlem8  49015  isubgr3stgrlem9  49016  grlimfn  49021  isgrlim  49024  uspgrlimlem1  49030  uspgrlimlem2  49031  uspgrlimlem3  49032  uspgrlimlem4  49033  grlimprclnbgredg  49039  grlimgredgex  49042  grlimgrtrilem2  49044  grlictr  49057  clnbgr3stgrgrlim  49061  clnbgr3stgrgrlic  49062  1hegrlfgr  49174  funcringcsetcALTV2lem8  49338  funcringcsetclem8ALTV  49361  itcovalendof  49725  uptrlem1  50262  uptr2  50273  swapf2f1oaALT  50330  swapfcoa  50333  swapffunc  50334  fucoppc  50462  thincciso  50505  thinccisod  50506  lmdran  50723  cmdlan  50724  amgmwlem  50931