Theorem f1of 6763

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

Syntax hints:   → wi 4  ⟶wf 6477  –1-1→wf1 6478  –1-1-onto→wf1o 6480

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 6486  df-f1o 6488

This theorem is referenced by:  f1ofn  6764  f1ompt  7044  f1oresrab  7060  fsn  7068  fsnunf  7119  f1ounsn  7206  f1ocnvfv1  7210  f1ocnvfv2  7211  fsnex  7217  f1ocnvdm  7219  fcof1oinvd  7227  fveqf1o  7236  isocnv  7264  isocnv3  7266  isores2  7267  isotr  7270  isofr2  7278  isopolem  7279  isosolem  7281  f1oiso2  7286  weniso  7288  f1ofveu  7340  f1oexrnex  7857  f1oabexg  7872  f1oabexgOLD  7873  wemoiso  7905  mptcnfimad  7918  suppsnop  8108  smoiso  8282  mapsnd  8810  ralxpmap  8820  f1oen2g  8891  en1  8946  enfixsn  8999  mapen  9054  ac6sfi  9168  domunfican  9206  fiint  9211  mapfienlem1  9289  mapfienlem2  9290  mapfienlem3  9291  mapfien  9292  supisoex  9359  supiso  9360  ordiso2  9401  unxpwdom2  9474  cantnfle  9561  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1d  9578  cantnflem1  9579  cnfcomlem  9589  cnfcom  9590  cnfcom2lem  9591  cnfcom2  9592  cnfcom3lem  9593  cnfcom3  9594  cnfcom3clem  9595  djuin  9808  infxpenlem  9901  infxpenc  9906  infxpenc2lem2  9908  fseqenlem1  9912  acndom  9939  acndom2  9942  infpwfien  9950  iunfictbso  10002  infmap2  10105  ackbij2lem2  10127  infpssrlem3  10193  infpssrlem4  10194  fin23lem30  10230  isf32lem6  10246  isf32lem7  10247  isf32lem8  10248  enfin1ai  10272  axcc3  10326  axcclem  10345  ttukeylem7  10403  fpwwe2lem5  10523  fpwwe2lem6  10524  fpwwe2lem8  10526  canthp1lem2  10541  canthp1  10542  pwfseqlem4a  10549  pwfseqlem5  10551  axdc4uzlem  13887  seqf1olem1  13945  seqf1olem2  13946  seqf1o  13947  hashkf  14236  hasheqf1oi  14255  hasheqf1od  14257  hashcl  14260  hashgadd  14281  hashfacen  14358  hashf1lem1  14359  fz1isolem  14365  seqcoll  14368  seqcoll2  14369  cnrecnv  15069  sumeq2ii  15597  summolem3  15618  summolem2a  15619  fsum  15624  fsumf1o  15627  fsumss  15629  fsumcl2lem  15635  fsumadd  15644  fsummulc2  15688  fsumrelem  15711  ackbijnn  15732  prodeq2ii  15815  prodmolem3  15837  prodmolem2a  15838  fprod  15845  fprodf1o  15850  fprodss  15852  fprodser  15853  fprodcl2lem  15854  fprodmul  15864  fproddiv  15865  fprodn0  15883  fproddvdsd  16243  sadcaddlem  16365  sadadd2lem  16367  sadadd3  16369  sadaddlem  16374  sadasslem  16378  sadeq  16380  phimullem  16687  eulerthlem1  16689  eulerthlem2  16690  unbenlem  16817  vdwlem8  16897  0ram  16929  wunndx  17103  xpsaddlem  17474  xpsvsca  17478  xpsle  17480  idfucl  17785  setccatid  17988  setcinv  17994  catcisolem  18014  estrccatid  18035  funcestrcsetclem7  18049  funcestrcsetclem8  18050  funcsetcestrclem7  18064  funcsetcestrclem8  18065  yonffthlem  18185  gsumpropd2lem  18584  mgmhmf1o  18605  idmgmhm  18606  idmhm  18700  mhmf1o  18701  gsumws1  18743  ielefmnd  18792  idghm  19141  ghmf1o  19158  symgbas  19282  elsymgbas  19284  symgbasf  19286  symgbasfi  19289  symg1bas  19301  symggrp  19310  lactghmga  19315  symgfixf1  19347  f1omvdmvd  19353  f1omvdconj  19356  f1omvdco2  19358  pmtrfconj  19376  symggen  19380  pmtrdifellem1  19386  pmtrdifellem2  19387  psgnunilem1  19403  gsumval3eu  19814  gsumval3lem1  19815  gsumval3  19817  gsumzf1o  19822  gsumconst  19844  gsumsub  19858  gsumcom2  19885  dprdfsub  19933  dprdf1o  19944  dprdsn  19948  ablfaclem2  19998  rngisomfv1  20381  rngisom1  20382  rngisomring1  20384  fidomndrnglem  20685  srngcl  20762  lmhmf1o  20978  gsumfsum  21369  zntoslem  21491  islinds2  21748  lindsmm  21763  psrass1lem  21867  psrnegcl  21889  psrlinv  21890  coe1f2  22120  coe1add  22176  evls1rhmlem  22234  evl1sca  22247  pf1ind  22268  mat1dimelbas  22384  mat1f  22395  mdetleib2  22501  mdetrsca  22516  mdetralt  22521  mdetunilem7  22531  mdetunilem9  22533  ssidcn  23168  hmphdis  23709  indishmph  23711  cmphaushmeo  23713  ordthmeolem  23714  txhmeo  23716  qtopf1  23729  ufldom  23875  symgtgp  24019  tsmsf1o  24058  iducn  24195  imasdsf1olem  24286  xpsdsval  24294  imasf1obl  24401  icchmeo  24863  icchmeoOLD  24864  iccpnfcnv  24867  xrhmeo  24869  cnheiborlem  24878  ovolctb  25416  ovoliunlem1  25428  ovoliunlem2  25429  iunmbl2  25483  dyadmbl  25526  vitalilem2  25535  vitalilem3  25536  vitalilem4  25537  vitalilem5  25538  mbfid  25561  dvid  25844  dvexp  25882  dvcnvlem  25905  dvcnv  25906  dvcnvrelem2  25948  dvcnvre  25949  efcvx  26384  reefgim  26385  efif1olem4  26479  eff1olem  26482  logrncl  26501  relogcl  26509  dvrelog  26571  relogcn  26572  logcn  26581  logf1o2  26584  dvlog  26585  dvlog2  26587  advlog  26588  advlogexp  26589  logtayl  26594  logccv  26597  dvcxp1  26674  loglesqrt  26696  asinrebnd  26836  dvatan  26870  efrlim  26904  efrlimOLD  26905  amgmlem  26925  lgamcvg2  26990  wilthlem2  27004  wilthlem3  27005  sqff1o  27117  lgsqrlem4  27285  logdivsum  27469  log2sumbnd  27480  isismt  28510  motcl  28515  motco  28516  cnvmot  28517  motgrp  28519  motcgrg  28520  f1otrg  28847  f1otrge  28848  axlowdimlem10  28927  axcontlem5  28944  axcontlem10  28949  uspgriedgedg  29152  upgrres1  29289  umgrres1  29290  upgriseupth  30182  pliguhgr  30461  dmadjrn  31870  unopnorm  31892  unopadj  31894  unoplin  31895  counop  31896  idcnop  31956  idhmop  31957  unopbd  31990  bracnln  32084  cnvbraval  32085  leopnmid  32113  nmopleid  32114  hmopidmch  32128  hmopidmpj  32129  disjrdx  32566  fmptco1f1o  32610  isoun  32678  padct  32696  fcobij  32698  fcobijfs  32699  fcobijfs2  32700  wrdpmcl  32914  ccatws1f1o  32927  ccatws1f1olast  32928  mndlactf1o  33006  mndractf1o  33007  abliso  33012  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  33327  ellspds  33328  1arithidomlem1  33495  1arithidomlem2  33496  1arithidom  33497  mplvrpmlem  33568  mplvrpmfgalem  33569  mplvrpmmhm  33571  mplvrpmrhm  33572  esplylem  33582  esplympl  33583  esplymhp  33584  esplyfv1  33585  esplyfv  33586  esplysply  33587  tpr2rico  33920  xrge0iifmhm  33947  xrge0pluscn  33948  rrhre  34029  esumf1o  34058  volmeas  34239  eulerpartgbij  34380  eulerpartlemmf  34383  eulerpartlemgvv  34384  eulerpartlemgf  34387  eulerpartlemgs2  34388  eulerpartlemn  34389  ballotlemsima  34524  reprpmtf1o  34634  logdivsqrle  34658  hgt750lemg  34662  vonf1owev  35140  deranglem  35198  derangsn  35202  derangenlem  35203  subfacp1lem4  35215  subfacp1lem5  35216  subfacp1lem6  35217  cvmfolem  35311  cvmliftlem6  35322  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem4  37663  poimirlem6  37665  poimirlem7  37666  poimirlem9  37668  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  poimirlem32  37691  mblfinlem2  37697  dvasin  37743  f1ocan1fv  37765  metf1o  37794  ismtyval  37839  isismty  37840  ismtyima  37842  ismtyhmeolem  37843  ismtybndlem  37845  ismrer1  37877  reheibor  37878  grposnOLD  37921  rngoisocnv  38020  lflnegl  39114  lautset  40120  islaut  40121  lautcl  40125  lautco  40135  pautsetN  40136  ispautN  40137  ldilco  40154  ltrncoidN  40166  ltrncoval  40183  trlcoabs2N  40760  trlcoat  40761  trlcone  40766  cdlemg47a  40772  cdlemg46  40773  cdlemg47  40774  trljco  40778  tgrpgrplem  40787  tendoidcl  40807  tendo0co2  40826  tendo0pl  40829  cdlemi2  40857  cdlemk2  40870  cdlemk4  40872  cdlemk8  40876  cdlemkid2  40962  cdlemk45  40985  cdlemk53b  40994  cdlemk53  40995  cdlemk55a  40997  erng1r  41033  tendocnv  41059  dvalveclem  41063  dva0g  41065  dvhgrp  41145  dvh0g  41149  dvhopN  41154  cdlemn3  41235  cdlemn8  41242  cdlemn9  41243  dihordlem7b  41253  dihopelvalcpre  41286  dihmeetlem1N  41328  dihglblem5apreN  41329  lcfrlem13  41593  hvmapclN  41802  hvmapcl2  41804  dvrelog2  42096  dvrelog3  42097  sticksstones3  42180  sticksstones17  42195  sticksstones18  42196  sticksstones19  42197  readvrec2  42393  readvrec  42394  mapfzcons  42748  mzpresrename  42782  diophrw  42791  eldioph2  42794  diophren  42845  kelac1  43095  imasgim  43132  lnrfg  43151  nvocnvb  43454  brco2f1o  44064  brco3f1o  44065  clsneikex  44138  clsneinex  44139  clsneiel1  44140  neicvgmex  44149  neicvgel1  44151  dssmapntrcls  44160  stoweidlem27  46064  stoweidlem31  46068  stoweidlem39  46076  fourierdlem20  46164  fourierdlem50  46193  fourierdlem52  46195  fourierdlem54  46197  fourierdlem64  46207  fourierdlem76  46219  fourierdlem102  46245  fourierdlem114  46257  sge0f1o  46419  nnfoctbdjlem  46492  isomenndlem  46567  ovnsubaddlem1  46607  3f1oss1  47105  reuf1odnf  47137  reuf1od  47138  f1oresf1o2  47321  fundcmpsurbijinjpreimafv  47437  fundcmpsurinjimaid  47441  grimfn  47909  isgrim  47912  grimuhgr  47917  grimco  47919  uhgrimedgi  47920  isuspgrim0lem  47923  isuspgrim0  47924  isuspgrim  47926  upgrimwlklem4  47930  gricushgr  47947  isubgrgrim  47959  uhgrimisgrgriclem  47960  uhgrimisgrgric  47961  clnbgrgrim  47964  grimedg  47965  grtriclwlk3  47975  isubgr3stgrlem3  47998  isubgr3stgrlem4  47999  isubgr3stgrlem6  48001  isubgr3stgrlem7  48002  isubgr3stgrlem8  48003  isubgr3stgrlem9  48004  grlimfn  48009  isgrlim  48012  uspgrlimlem1  48018  uspgrlimlem2  48019  uspgrlimlem3  48020  uspgrlimlem4  48021  grlimprclnbgredg  48027  grlimgredgex  48030  grlimgrtrilem2  48032  grlictr  48045  clnbgr3stgrgrlim  48049  clnbgr3stgrgrlic  48050  1hegrlfgr  48162  funcringcsetcALTV2lem8  48327  funcringcsetclem8ALTV  48350  itcovalendof  48700  uptrlem1  49241  uptr2  49252  swapf2f1oaALT  49309  swapfcoa  49312  swapffunc  49313  fucoppc  49441  thincciso  49484  thinccisod  49485  lmdran  49702  cmdlan  49703  amgmwlem  49833