Theorem f1of 6774

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

Syntax hints:   → wi 4  ⟶wf 6488  –1-1→wf1 6489  –1-1-onto→wf1o 6491

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 6497  df-f1o 6499

This theorem is referenced by:  f1ofn  6775  f1ompt  7056  f1oresrab  7072  fsn  7080  fsnunf  7131  f1ounsn  7218  f1ocnvfv1  7222  f1ocnvfv2  7223  fsnex  7229  f1ocnvdm  7231  fcof1oinvd  7239  fveqf1o  7248  isocnv  7276  isocnv3  7278  isores2  7279  isotr  7282  isofr2  7290  isopolem  7291  isosolem  7293  f1oiso2  7298  weniso  7300  f1ofveu  7352  f1oexrnex  7869  f1oabexg  7884  f1oabexgOLD  7885  wemoiso  7917  mptcnfimad  7930  suppsnop  8120  smoiso  8294  mapsnd  8824  ralxpmap  8834  f1oen2g  8905  en1  8961  enfixsn  9014  mapen  9069  ac6sfi  9184  domunfican  9222  fiint  9227  mapfienlem1  9308  mapfienlem2  9309  mapfienlem3  9310  mapfien  9311  supisoex  9378  supiso  9379  ordiso2  9420  unxpwdom2  9493  cantnfle  9580  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1d  9597  cantnflem1  9598  cnfcomlem  9608  cnfcom  9609  cnfcom2lem  9610  cnfcom2  9611  cnfcom3lem  9612  cnfcom3  9613  cnfcom3clem  9614  djuin  9830  infxpenlem  9923  infxpenc  9928  infxpenc2lem2  9930  fseqenlem1  9934  acndom  9961  acndom2  9964  infpwfien  9972  iunfictbso  10024  infmap2  10127  ackbij2lem2  10149  infpssrlem3  10215  infpssrlem4  10216  fin23lem30  10252  isf32lem6  10268  isf32lem7  10269  isf32lem8  10270  enfin1ai  10294  axcc3  10348  axcclem  10367  ttukeylem7  10425  fpwwe2lem5  10546  fpwwe2lem6  10547  fpwwe2lem8  10549  canthp1lem2  10564  canthp1  10565  pwfseqlem4a  10572  pwfseqlem5  10574  axdc4uzlem  13906  seqf1olem1  13964  seqf1olem2  13965  seqf1o  13966  hashkf  14255  hasheqf1oi  14274  hasheqf1od  14276  hashcl  14279  hashgadd  14300  hashfacen  14377  hashf1lem1  14378  fz1isolem  14384  seqcoll  14387  seqcoll2  14388  cnrecnv  15088  sumeq2ii  15616  summolem3  15637  summolem2a  15638  fsum  15643  fsumf1o  15646  fsumss  15648  fsumcl2lem  15654  fsumadd  15663  fsummulc2  15707  fsumrelem  15730  ackbijnn  15751  prodeq2ii  15834  prodmolem3  15856  prodmolem2a  15857  fprod  15864  fprodf1o  15869  fprodss  15871  fprodser  15872  fprodcl2lem  15873  fprodmul  15883  fproddiv  15884  fprodn0  15902  fproddvdsd  16262  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  sadasslem  16397  sadeq  16399  phimullem  16706  eulerthlem1  16708  eulerthlem2  16709  unbenlem  16836  vdwlem8  16916  0ram  16948  wunndx  17122  xpsaddlem  17494  xpsvsca  17498  xpsle  17500  idfucl  17805  setccatid  18008  setcinv  18014  catcisolem  18034  estrccatid  18055  funcestrcsetclem7  18069  funcestrcsetclem8  18070  funcsetcestrclem7  18084  funcsetcestrclem8  18085  yonffthlem  18205  gsumpropd2lem  18604  mgmhmf1o  18625  idmgmhm  18626  idmhm  18720  mhmf1o  18721  gsumws1  18763  ielefmnd  18812  idghm  19160  ghmf1o  19177  symgbas  19301  elsymgbas  19303  symgbasf  19305  symgbasfi  19308  symg1bas  19320  symggrp  19329  lactghmga  19334  symgfixf1  19366  f1omvdmvd  19372  f1omvdconj  19375  f1omvdco2  19377  pmtrfconj  19395  symggen  19399  pmtrdifellem1  19405  pmtrdifellem2  19406  psgnunilem1  19422  gsumval3eu  19833  gsumval3lem1  19834  gsumval3  19836  gsumzf1o  19841  gsumconst  19863  gsumsub  19877  gsumcom2  19904  dprdfsub  19952  dprdf1o  19963  dprdsn  19967  ablfaclem2  20017  rngisomfv1  20401  rngisom1  20402  rngisomring1  20404  fidomndrnglem  20705  srngcl  20782  lmhmf1o  20998  gsumfsum  21389  zntoslem  21511  islinds2  21768  lindsmm  21783  psrass1lem  21888  psrnegcl  21910  psrlinv  21911  coe1f2  22150  coe1add  22206  evls1rhmlem  22265  evl1sca  22278  pf1ind  22299  mat1dimelbas  22415  mat1f  22426  mdetleib2  22532  mdetrsca  22547  mdetralt  22552  mdetunilem7  22562  mdetunilem9  22564  ssidcn  23199  hmphdis  23740  indishmph  23742  cmphaushmeo  23744  ordthmeolem  23745  txhmeo  23747  qtopf1  23760  ufldom  23906  symgtgp  24050  tsmsf1o  24089  iducn  24226  imasdsf1olem  24317  xpsdsval  24325  imasf1obl  24432  icchmeo  24894  icchmeoOLD  24895  iccpnfcnv  24898  xrhmeo  24900  cnheiborlem  24909  ovolctb  25447  ovoliunlem1  25459  ovoliunlem2  25460  iunmbl2  25514  dyadmbl  25557  vitalilem2  25566  vitalilem3  25567  vitalilem4  25568  vitalilem5  25569  mbfid  25592  dvid  25875  dvexp  25913  dvcnvlem  25936  dvcnv  25937  dvcnvrelem2  25979  dvcnvre  25980  efcvx  26415  reefgim  26416  efif1olem4  26510  eff1olem  26513  logrncl  26532  relogcl  26540  dvrelog  26602  relogcn  26603  logcn  26612  logf1o2  26615  dvlog  26616  dvlog2  26618  advlog  26619  advlogexp  26620  logtayl  26625  logccv  26628  dvcxp1  26705  loglesqrt  26727  asinrebnd  26867  dvatan  26901  efrlim  26935  efrlimOLD  26936  amgmlem  26956  lgamcvg2  27021  wilthlem2  27035  wilthlem3  27036  sqff1o  27148  lgsqrlem4  27316  logdivsum  27500  log2sumbnd  27511  isismt  28606  motcl  28611  motco  28612  cnvmot  28613  motgrp  28615  motcgrg  28616  f1otrg  28943  f1otrge  28944  axlowdimlem10  29024  axcontlem5  29041  axcontlem10  29046  uspgriedgedg  29249  upgrres1  29386  umgrres1  29387  upgriseupth  30282  pliguhgr  30561  dmadjrn  31970  unopnorm  31992  unopadj  31994  unoplin  31995  counop  31996  idcnop  32056  idhmop  32057  unopbd  32090  bracnln  32184  cnvbraval  32185  leopnmid  32213  nmopleid  32214  hmopidmch  32228  hmopidmpj  32229  disjrdx  32666  fmptco1f1o  32711  isoun  32781  padct  32797  fcobij  32799  fcobijfs  32800  fcobijfs2  32801  wrdpmcl  33020  ccatws1f1o  33033  ccatws1f1olast  33034  mndlactf1o  33112  mndractf1o  33113  abliso  33118  symgfcoeu  33164  symgcom  33165  pmtrcnel  33171  pmtrcnel2  33172  pmtrcnelor  33173  wrdpmtrlast  33175  cycpmco2f1  33206  cycpmco2rn  33207  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  cycpmconjv  33224  cycpmconjslem1  33236  cycpmconjslem2  33237  cycpmconjs  33238  islinds5  33448  ellspds  33449  1arithidomlem1  33616  1arithidomlem2  33617  1arithidom  33618  mplvrpmlem  33708  mplvrpmfgalem  33709  mplvrpmmhm  33711  mplvrpmrhm  33712  esplyfval0  33722  esplylem  33724  esplympl  33725  esplymhp  33726  esplyfv1  33727  esplyfv  33728  esplysply  33729  esplyfval3  33730  vieta  33736  tpr2rico  34069  xrge0iifmhm  34096  xrge0pluscn  34097  rrhre  34178  esumf1o  34207  volmeas  34388  eulerpartgbij  34529  eulerpartlemmf  34532  eulerpartlemgvv  34533  eulerpartlemgf  34536  eulerpartlemgs2  34537  eulerpartlemn  34538  ballotlemsima  34673  reprpmtf1o  34783  logdivsqrle  34807  hgt750lemg  34811  vonf1owev  35302  deranglem  35360  derangsn  35364  derangenlem  35365  subfacp1lem4  35377  subfacp1lem5  35378  subfacp1lem6  35379  cvmfolem  35473  cvmliftlem6  35484  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem4  37821  poimirlem6  37823  poimirlem7  37824  poimirlem9  37826  poimirlem11  37828  poimirlem12  37829  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem22  37839  poimirlem26  37843  poimirlem27  37844  poimirlem28  37845  poimirlem32  37849  mblfinlem2  37855  dvasin  37901  f1ocan1fv  37923  metf1o  37952  ismtyval  37997  isismty  37998  ismtyima  38000  ismtyhmeolem  38001  ismtybndlem  38003  ismrer1  38035  reheibor  38036  grposnOLD  38079  rngoisocnv  38178  lflnegl  39332  lautset  40338  islaut  40339  lautcl  40343  lautco  40353  pautsetN  40354  ispautN  40355  ldilco  40372  ltrncoidN  40384  ltrncoval  40401  trlcoabs2N  40978  trlcoat  40979  trlcone  40984  cdlemg47a  40990  cdlemg46  40991  cdlemg47  40992  trljco  40996  tgrpgrplem  41005  tendoidcl  41025  tendo0co2  41044  tendo0pl  41047  cdlemi2  41075  cdlemk2  41088  cdlemk4  41090  cdlemk8  41094  cdlemkid2  41180  cdlemk45  41203  cdlemk53b  41212  cdlemk53  41213  cdlemk55a  41215  erng1r  41251  tendocnv  41277  dvalveclem  41281  dva0g  41283  dvhgrp  41363  dvh0g  41367  dvhopN  41372  cdlemn3  41453  cdlemn8  41460  cdlemn9  41461  dihordlem7b  41471  dihopelvalcpre  41504  dihmeetlem1N  41546  dihglblem5apreN  41547  lcfrlem13  41811  hvmapclN  42020  hvmapcl2  42022  dvrelog2  42314  dvrelog3  42315  sticksstones3  42398  sticksstones17  42413  sticksstones18  42414  sticksstones19  42415  readvrec2  42612  readvrec  42613  mapfzcons  42954  mzpresrename  42988  diophrw  42997  eldioph2  43000  diophren  43051  kelac1  43301  imasgim  43338  lnrfg  43357  nvocnvb  43659  brco2f1o  44269  brco3f1o  44270  clsneikex  44343  clsneinex  44344  clsneiel1  44345  neicvgmex  44354  neicvgel1  44356  dssmapntrcls  44365  stoweidlem27  46267  stoweidlem31  46271  stoweidlem39  46279  fourierdlem20  46367  fourierdlem50  46396  fourierdlem52  46398  fourierdlem54  46400  fourierdlem64  46410  fourierdlem76  46422  fourierdlem102  46448  fourierdlem114  46460  sge0f1o  46622  nnfoctbdjlem  46695  isomenndlem  46770  ovnsubaddlem1  46810  3f1oss1  47317  reuf1odnf  47349  reuf1od  47350  f1oresf1o2  47533  fundcmpsurbijinjpreimafv  47649  fundcmpsurinjimaid  47653  grimfn  48121  isgrim  48124  grimuhgr  48129  grimco  48131  uhgrimedgi  48132  isuspgrim0lem  48135  isuspgrim0  48136  isuspgrim  48138  upgrimwlklem4  48142  gricushgr  48159  isubgrgrim  48171  uhgrimisgrgriclem  48172  uhgrimisgrgric  48173  clnbgrgrim  48176  grimedg  48177  grtriclwlk3  48187  isubgr3stgrlem3  48210  isubgr3stgrlem4  48211  isubgr3stgrlem6  48213  isubgr3stgrlem7  48214  isubgr3stgrlem8  48215  isubgr3stgrlem9  48216  grlimfn  48221  isgrlim  48224  uspgrlimlem1  48230  uspgrlimlem2  48231  uspgrlimlem3  48232  uspgrlimlem4  48233  grlimprclnbgredg  48239  grlimgredgex  48242  grlimgrtrilem2  48244  grlictr  48257  clnbgr3stgrgrlim  48261  clnbgr3stgrgrlic  48262  1hegrlfgr  48374  funcringcsetcALTV2lem8  48539  funcringcsetclem8ALTV  48562  itcovalendof  48911  uptrlem1  49451  uptr2  49462  swapf2f1oaALT  49519  swapfcoa  49522  swapffunc  49523  fucoppc  49651  thincciso  49694  thinccisod  49695  lmdran  49912  cmdlan  49913  amgmwlem  50043