Theorem f1of 6827

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

This proof depends on syntax axioms:   → wi 4  ⟶wf 6539  –1-1→wf1 6540  –1-1-onto→wf1o 6542

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 6548  df-f1o 6550

This theorem is used by:  f1ofn  6828  f1ompt  7113  f1oresrab  7130  fsn  7138  fsnunf  7190  f1ounsn  7281  f1ocnvfv1  7285  f1ocnvfv2  7286  fsnex  7292  f1ocnvdm  7294  fcof1oinvd  7302  fveqf1o  7311  isocnv  7339  isocnv3  7341  isores2  7342  isotr  7345  isofr2  7353  isopolem  7354  isosolem  7356  f1oiso2  7361  weniso  7365  f1ofveu  7417  f1oexrnex  7933  f1oabexg  7947  wemoiso  7979  mptcnfimad  7992  suppsnop  8183  smoiso  8358  mapsnd  8893  ralxpmap  8903  f1oen2g  8974  en1  9030  enfixsn  9084  mapen  9139  ac6sfi  9254  domunfican  9291  fiint  9296  mapfienlem1  9375  mapfienlem2  9376  mapfienlem3  9377  mapfien  9378  supisoex  9445  supiso  9446  ordiso2  9487  unxpwdom2  9560  cantnfle  9650  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1d  9667  cantnflem1  9668  cnfcomlem  9678  cnfcom  9679  cnfcom2lem  9680  cnfcom2  9681  cnfcom3lem  9682  cnfcom3  9683  cnfcom3clem  9684  djuin  9923  infxpenlem  10016  infxpenc  10021  infxpenc2lem2  10023  fseqenlem1  10027  acndom  10054  acndom2  10057  infpwfien  10065  iunfictbso  10117  infmap2  10219  ackbij2lem2  10241  infpssrlem3  10307  infpssrlem4  10308  fin23lem30  10344  isf32lem6  10360  isf32lem7  10361  isf32lem8  10362  enfin1ai  10386  axcc3  10440  axcclem  10459  ttukeylem7  10517  fpwwe2lem5  10638  fpwwe2lem6  10639  fpwwe2lem8  10641  canthp1lem2  10656  canthp1  10657  pwfseqlem4a  10664  pwfseqlem5  10666  axdc4uzlem  14039  seqf1olem1  14097  seqf1olem2  14098  seqf1o  14099  hashkf  14388  hasheqf1oi  14407  hasheqf1od  14409  hashcl  14412  hashgadd  14433  hashfacen  14511  hashf1lem1  14512  fz1isolem  14518  seqcoll  14521  seqcoll2  14522  cnrecnv  15242  sumeq2ii  15770  summolem3  15791  summolem2a  15792  fsum  15797  fsumf1o  15800  fsumss  15802  fsumcl2lem  15808  fsumadd  15817  fsummulc2  15861  fsumrelem  15885  ackbijnn  15908  prodeq2ii  15991  prodmolem3  16013  prodmolem2a  16014  fprod  16021  fprodf1o  16026  fprodss  16028  fprodser  16029  fprodcl2lem  16030  fprodmul  16040  fproddiv  16041  fprodn0  16059  fproddvdsd  16418  sadcaddlem  16540  sadadd2lem  16542  sadadd3  16544  sadaddlem  16549  sadasslem  16553  sadeq  16555  phimullem  16863  eulerthlem1  16865  eulerthlem2  16866  unbenlem  16993  vdwlem8  17073  0ram  17105  wunndx  17280  xpsaddlem  17652  xpsvsca  17656  xpsle  17658  idfucl  17963  setccatid  18166  setcinv  18172  catcisolem  18192  estrccatid  18213  funcestrcsetclem7  18227  funcestrcsetclem8  18228  funcsetcestrclem7  18242  funcsetcestrclem8  18243  yonffthlem  18363  gsumpropd2lem  18766  mgmhmf1o  18787  idmgmhm  18788  idmhm  18884  mhmf1o  18885  gsumws1  18928  ielefmnd  18977  idghm  19332  ghmf1o  19349  symgbas  19473  elsymgbas  19475  symgbasf  19477  symgbasfi  19480  symg1bas  19492  symggrp  19501  lactghmga  19506  symgfixf1  19538  f1omvdmvd  19544  f1omvdconj  19547  f1omvdco2  19549  pmtrfconj  19567  symggen  19571  pmtrdifellem1  19577  pmtrdifellem2  19578  psgnunilem1  19594  gsumval3eu  20005  gsumval3lem1  20006  gsumval3  20008  gsumzf1o  20013  gsumconst  20035  gsumsub  20049  gsumcom2  20076  dprdfsub  20124  dprdf1o  20135  dprdsn  20139  ablfaclem2  20189  rngisomfv1  20580  rngisom1  20581  rngisomring1  20583  fidomndrnglem  20913  srngcl  20989  lmhmf1o  21204  gsumfsum  21621  zntoslem  21743  islinds2  22000  lindsmm  22015  psrass1lem  22120  psrnegcl  22141  psrlinv  22142  coe1f2  22406  coe1add  22462  evls1rhmlem  22518  evl1sca  22531  pf1ind  22552  mat1dimelbas  22665  mat1f  22676  mdetleib2  22782  mdetrsca  22797  mdetralt  22802  mdetunilem7  22812  mdetunilem9  22814  ssidcn  23449  hmphdis  23990  indishmph  23992  cmphaushmeo  23994  ordthmeolem  23995  txhmeo  23997  qtopf1  24010  ufldom  24156  symgtgp  24300  tsmsf1o  24339  iducn  24476  imasdsf1olem  24567  xpsdsval  24575  imasf1obl  24682  icchmeo  25137  iccpnfcnv  25140  xrhmeo  25142  cnheiborlem  25150  ovolctb  25686  ovoliunlem1  25698  ovoliunlem2  25699  iunmbl2  25753  dyadmbl  25796  vitalilem2  25805  vitalilem3  25806  vitalilem4  25807  vitalilem5  25808  mbfid  25831  dvid  26114  dvexp  26149  dvcnvlem  26172  dvcnv  26173  dvcnvrelem2  26214  dvcnvre  26215  efcvx  26649  reefgim  26650  efif1olem4  26747  eff1olem  26750  logrncl  26769  relogcl  26777  dvrelog  26839  relogcn  26840  logcn  26849  logf1o2  26852  dvlog  26853  dvlog2  26855  advlog  26856  advlogexp  26857  logtayl  26862  logccv  26865  dvcxp1  26942  loglesqrt  26963  asinrebnd  27103  dvatan  27137  efrlim  27171  amgmlem  27191  lgamcvg2  27256  wilthlem2  27270  wilthlem3  27271  sqff1o  27383  lgsqrlem4  27550  logdivsum  27734  log2sumbnd  27745  isismt  28840  motcl  28845  motco  28846  cnvmot  28847  motgrp  28849  motcgrg  28850  f1otrg  29257  f1otrge  29258  axlowdimlem10  29338  axcontlem5  29355  axcontlem10  29360  uspgriedgedg  29563  upgrres1  29700  umgrres1  29701  upgriseupth  30595  pliguhgr  30875  dmadjrn  32284  unopnorm  32306  unopadj  32308  unoplin  32309  counop  32310  idcnop  32370  idhmop  32371  unopbd  32404  bracnln  32498  cnvbraval  32499  leopnmid  32527  nmopleid  32528  hmopidmch  32542  hmopidmpj  32543  disjrdx  32973  fmptco1f1o  33015  isoun  33084  padct  33100  fcobij  33102  fcobijfs  33103  fcobijfs2  33104  wrdpmcl  33295  ccatws1f1o  33304  ccatws1f1olast  33305  mndlactf1o  33381  mndractf1o  33382  abliso  33386  symgfcoeu  33433  symgcom  33434  pmtrcnel  33440  pmtrcnel2  33441  pmtrcnelor  33442  wrdpmtrlast  33444  cycpmco2f1  33475  cycpmco2rn  33476  cycpmco2lem2  33478  cycpmco2lem3  33479  cycpmco2lem4  33480  cycpmco2lem5  33481  cycpmco2lem6  33482  cycpmco2lem7  33483  cycpmco2  33484  cycpmconjv  33493  cycpmconjslem1  33505  cycpmconjslem2  33506  cycpmconjs  33507  islinds5  33713  ellspds  33714  1arithidomlem1  33856  1arithidomlem2  33857  1arithidom  33858  0mplrim  33935  selvply1rhmlemb  33940  mplvrpmlem  33964  mplvrpmfgalem  33965  mplvrpmmhm  33967  mplvrpmrhm  33968  esplyfval0  33985  esplylem  33987  esplympl  33988  esplymhp  33989  esplyfv1  33990  esplyfv  33991  esplysply  33992  esplyfval3  33993  vieta  34001  tpr2rico  34333  xrge0iifmhm  34360  xrge0pluscn  34361  rrhre  34442  esumf1o  34471  volmeas  34652  eulerpartgbij  34793  eulerpartlemmf  34796  eulerpartlemgvv  34797  eulerpartlemgf  34800  eulerpartlemgs2  34801  eulerpartlemn  34802  ballotlemsima  34937  reprpmtf1o  35044  logdivsqrle  35068  hgt750lemg  35072  vonf1owevOLD  35617  deranglem  35678  derangsn  35682  derangenlem  35683  subfacp1lem4  35695  subfacp1lem5  35696  subfacp1lem6  35697  cvmfolem  35791  cvmliftlem6  35802  poimirlem1  38312  poimirlem2  38313  poimirlem3  38314  poimirlem4  38315  poimirlem6  38317  poimirlem7  38318  poimirlem9  38320  poimirlem11  38322  poimirlem12  38323  poimirlem16  38327  poimirlem17  38328  poimirlem19  38330  poimirlem20  38331  poimirlem22  38333  poimirlem26  38337  poimirlem27  38338  poimirlem28  38339  poimirlem32  38343  mblfinlem2  38349  dvasin  38395  f1ocan1fv  38417  metf1o  38446  ismtyval  38491  isismty  38492  ismtyima  38494  ismtyhmeolem  38495  ismtybndlem  38497  ismrer1  38529  reheibor  38530  grposnOLD  38573  rngoisocnv  38672  lflnegl  39890  lautset  40896  islaut  40897  lautcl  40901  lautco  40911  pautsetN  40912  ispautN  40913  ldilco  40930  ltrncoidN  40942  ltrncoval  40959  trlcoabs2N  41536  trlcoat  41537  trlcone  41542  cdlemg47a  41548  cdlemg46  41549  cdlemg47  41550  trljco  41554  tgrpgrplem  41563  tendoidcl  41583  tendo0co2  41602  tendo0pl  41605  cdlemi2  41633  cdlemk2  41646  cdlemk4  41648  cdlemk8  41652  cdlemkid2  41738  cdlemk45  41761  cdlemk53b  41770  cdlemk53  41771  cdlemk55a  41773  erng1r  41809  tendocnv  41835  dvalveclem  41839  dva0g  41841  dvhgrp  41921  dvh0g  41925  dvhopN  41930  cdlemn3  42011  cdlemn8  42018  cdlemn9  42019  dihordlem7b  42029  dihopelvalcpre  42062  dihmeetlem1N  42104  dihglblem5apreN  42105  lcfrlem13  42369  hvmapclN  42578  hvmapcl2  42580  dvrelog2  42871  dvrelog3  42872  sticksstones3  42955  sticksstones17  42970  sticksstones18  42971  sticksstones19  42972  readvrec2  43162  readvrec  43163  mapfzcons  43487  mzpresrename  43521  diophrw  43530  eldioph2  43533  diophren  43580  kelac1  43830  imasgim  43867  lnrfg  43886  nvocnvb  44188  brco2f1o  44798  brco3f1o  44799  clsneikex  44872  clsneinex  44873  clsneiel1  44874  neicvgmex  44883  neicvgel1  44885  dssmapntrcls  44894  stoweidlem27  46781  stoweidlem31  46785  stoweidlem39  46793  fourierdlem20  46881  fourierdlem50  46910  fourierdlem52  46912  fourierdlem54  46914  fourierdlem64  46924  fourierdlem76  46936  fourierdlem102  46962  fourierdlem114  46974  sge0f1o  47136  nnfoctbdjlem  47209  isomenndlem  47284  ovnsubaddlem1  47324  3f1oss1  47852  reuf1odnf  47884  reuf1od  47885  f1oresf1o2  48068  fundcmpsurbijinjpreimafv  48196  fundcmpsurinjimaid  48200  grimfn  48684  isgrim  48687  grimuhgr  48692  grimco  48694  uhgrimedgi  48695  isuspgrim0lem  48698  isuspgrim0  48699  isuspgrim  48701  upgrimwlklem4  48705  gricushgr  48722  isubgrgrim  48734  uhgrimisgrgriclem  48735  uhgrimisgrgric  48736  clnbgrgrim  48739  grimedg  48740  grtriclwlk3  48750  isubgr3stgrlem3  48773  isubgr3stgrlem4  48774  isubgr3stgrlem6  48776  isubgr3stgrlem7  48777  isubgr3stgrlem8  48778  isubgr3stgrlem9  48779  grlimfn  48784  isgrlim  48787  uspgrlimlem1  48793  uspgrlimlem2  48794  uspgrlimlem3  48795  uspgrlimlem4  48796  grlimprclnbgredg  48802  grlimgredgex  48805  grlimgrtrilem2  48807  grlictr  48820  clnbgr3stgrgrlim  48824  clnbgr3stgrgrlic  48825  1hegrlfgr  48937  funcringcsetcALTV2lem8  49102  funcringcsetclem8ALTV  49125  itcovalendof  49489  uptrlem1  50028  uptr2  50039  swapf2f1oaALT  50096  swapfcoa  50099  swapffunc  50100  fucoppc  50228  thincciso  50271  thinccisod  50272  lmdran  50489  cmdlan  50490  amgmwlem  50690