Theorem f1of 6838

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

Syntax hints:   → wi 4  ⟶wf 6545  –1-1→wf1 6546  –1-1-onto→wf1o 6548

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 206  df-an 395  df-f1 6554  df-f1o 6556

This theorem is referenced by:  f1ofn  6839  f1ompt  7120  f1oresrab  7136  fsn  7144  fsnunf  7194  f1ocnvfv1  7285  f1ocnvfv2  7286  fsnex  7292  f1ocnvdm  7294  fcof1oinvd  7302  fveqf1o  7311  isocnv  7337  isocnv3  7339  isores2  7340  isotr  7343  isofr2  7351  isopolem  7352  isosolem  7354  f1oiso2  7359  weniso  7361  f1ofveu  7413  f1oexrnex  7935  f1oabexg  7945  wemoiso  7978  mptcnfimad  7991  suppsnop  8183  smoiso  8383  mapsnd  8905  ralxpmap  8915  f1oen2g  8989  en1  9046  en1OLD  9047  enfixsn  9106  mapen  9166  ac6sfi  9312  domunfican  9346  fiint  9350  mapfienlem1  9430  mapfienlem2  9431  mapfienlem3  9432  mapfien  9433  supisoex  9499  supiso  9500  ordiso2  9540  unxpwdom2  9613  cantnfle  9696  cantnfp1lem3  9705  cantnflem1b  9711  cantnflem1d  9713  cantnflem1  9714  cnfcomlem  9724  cnfcom  9725  cnfcom2lem  9726  cnfcom2  9727  cnfcom3lem  9728  cnfcom3  9729  cnfcom3clem  9730  djuin  9943  infxpenlem  10038  infxpenc  10043  infxpenc2lem2  10045  fseqenlem1  10049  acndom  10076  acndom2  10079  infpwfien  10087  iunfictbso  10139  infmap2  10243  ackbij2lem2  10265  infpssrlem3  10330  infpssrlem4  10331  fin23lem30  10367  isf32lem6  10383  isf32lem7  10384  isf32lem8  10385  enfin1ai  10409  axcc3  10463  axcclem  10482  ttukeylem7  10540  fpwwe2lem5  10660  fpwwe2lem6  10661  fpwwe2lem8  10663  canthp1lem2  10678  canthp1  10679  pwfseqlem4a  10686  pwfseqlem5  10688  axdc4uzlem  13984  seqf1olem1  14042  seqf1olem2  14043  seqf1o  14044  hashkf  14327  hasheqf1oi  14346  hasheqf1od  14348  hashcl  14351  hashgadd  14372  hashfacen  14449  hashfacenOLD  14450  hashf1lem1  14451  hashf1lem1OLD  14452  fz1isolem  14458  seqcoll  14461  seqcoll2  14462  cnrecnv  15148  sumeq2ii  15675  summolem3  15696  summolem2a  15697  fsum  15702  fsumf1o  15705  fsumss  15707  fsumcl2lem  15713  fsumadd  15722  fsummulc2  15766  fsumrelem  15789  ackbijnn  15810  prodeq2ii  15893  prodmolem3  15913  prodmolem2a  15914  fprod  15921  fprodf1o  15926  fprodss  15928  fprodser  15929  fprodcl2lem  15930  fprodmul  15940  fproddiv  15941  fprodn0  15959  fproddvdsd  16315  sadcaddlem  16435  sadadd2lem  16437  sadadd3  16439  sadaddlem  16444  sadasslem  16448  sadeq  16450  phimullem  16751  eulerthlem1  16753  eulerthlem2  16754  unbenlem  16880  vdwlem8  16960  0ram  16992  wunndx  17167  xpsaddlem  17558  xpsvsca  17562  xpsle  17564  idfucl  17870  setccatid  18076  setcinv  18082  catcisolem  18102  estrccatid  18125  funcestrcsetclem7  18140  funcestrcsetclem8  18141  funcsetcestrclem7  18155  funcsetcestrclem8  18156  yonffthlem  18277  gsumpropd2lem  18642  mgmhmf1o  18663  idmgmhm  18664  idmhm  18755  mhmf1o  18756  gsumws1  18798  ielefmnd  18847  idghm  19194  ghmf1o  19211  permsetexOLD  19336  symgbas  19337  elsymgbas  19340  symgbasf  19342  symgbasfi  19345  symg1bas  19357  symggrp  19367  lactghmga  19372  symgfixf1  19404  f1omvdmvd  19410  f1omvdconj  19413  f1omvdco2  19415  pmtrfconj  19433  symggen  19437  pmtrdifellem1  19443  pmtrdifellem2  19444  psgnunilem1  19460  gsumval3eu  19871  gsumval3lem1  19872  gsumval3  19874  gsumzf1o  19879  gsumconst  19901  gsumsub  19915  gsumcom2  19942  dprdfsub  19990  dprdf1o  20001  dprdsn  20005  ablfaclem2  20055  rngisomfv1  20416  rngisom1  20417  rngisomring1  20419  srngcl  20747  lmhmf1o  20943  fidomndrnglem  21277  gsumfsum  21384  zntoslem  21507  islinds2  21764  lindsmm  21779  psrass1lemOLD  21891  psrass1lem  21894  psrnegcl  21916  psrlinv  21917  coe1f2  22152  coe1add  22208  evls1rhmlem  22265  evl1sca  22278  pf1ind  22299  mat1dimelbas  22417  mat1f  22428  mdetleib2  22534  mdetrsca  22549  mdetralt  22554  mdetunilem7  22564  mdetunilem9  22566  ssidcn  23203  hmphdis  23744  indishmph  23746  cmphaushmeo  23748  ordthmeolem  23749  txhmeo  23751  qtopf1  23764  ufldom  23910  symgtgp  24054  tsmsf1o  24093  iducn  24232  imasdsf1olem  24323  xpsdsval  24331  imasf1obl  24441  icchmeo  24909  icchmeoOLD  24910  iccpnfcnv  24913  xrhmeo  24915  cnheiborlem  24924  ovolctb  25463  ovoliunlem1  25475  ovoliunlem2  25476  iunmbl2  25530  dyadmbl  25573  vitalilem2  25582  vitalilem3  25583  vitalilem4  25584  vitalilem5  25585  mbfid  25608  dvid  25891  dvexp  25929  dvcnvlem  25952  dvcnv  25953  dvcnvrelem2  25995  dvcnvre  25996  efcvx  26431  reefgim  26432  efif1olem4  26524  eff1olem  26527  logrncl  26546  relogcl  26554  dvrelog  26616  relogcn  26617  logcn  26626  logf1o2  26629  dvlog  26630  dvlog2  26632  advlog  26633  advlogexp  26634  logtayl  26639  logccv  26642  dvcxp1  26719  loglesqrt  26738  asinrebnd  26878  dvatan  26912  efrlim  26946  efrlimOLD  26947  amgmlem  26967  lgamcvg2  27032  wilthlem2  27046  wilthlem3  27047  sqff1o  27159  lgsqrlem4  27327  logdivsum  27511  log2sumbnd  27522  isismt  28410  motcl  28415  motco  28416  cnvmot  28417  motgrp  28419  motcgrg  28420  f1otrg  28747  f1otrge  28748  axlowdimlem10  28834  axcontlem5  28851  axcontlem10  28856  uspgriedgedg  29061  upgrres1  29198  umgrres1  29199  upgriseupth  30089  pliguhgr  30368  dmadjrn  31777  unopnorm  31799  unopadj  31801  unoplin  31802  counop  31803  idcnop  31863  idhmop  31864  unopbd  31897  bracnln  31991  cnvbraval  31992  leopnmid  32020  nmopleid  32021  hmopidmch  32035  hmopidmpj  32036  disjrdx  32460  fmptco1f1o  32499  isoun  32563  padct  32583  fcobij  32586  fcobijfs  32587  wrdpmcl  32748  ccatws1f1o  32761  ccatws1f1olast  32762  abliso  32845  symgfcoeu  32895  symgcom  32896  pmtrcnel  32902  pmtrcnel2  32903  pmtrcnelor  32904  wrdpmtrlast  32906  cycpmco2f1  32937  cycpmco2rn  32938  cycpmco2lem2  32940  cycpmco2lem3  32941  cycpmco2lem4  32942  cycpmco2lem5  32943  cycpmco2lem6  32944  cycpmco2lem7  32945  cycpmco2  32946  cycpmconjv  32955  cycpmconjslem1  32967  cycpmconjslem2  32968  cycpmconjs  32969  islinds5  33178  ellspds  33179  1arithidomlem1  33347  1arithidomlem2  33348  1arithidom  33349  tpr2rico  33641  xrge0iifmhm  33668  xrge0pluscn  33669  rrhre  33750  esumf1o  33797  volmeas  33978  eulerpartgbij  34120  eulerpartlemmf  34123  eulerpartlemgvv  34124  eulerpartlemgf  34127  eulerpartlemgs2  34128  eulerpartlemn  34129  ballotlemsima  34263  reprpmtf1o  34386  logdivsqrle  34410  hgt750lemg  34414  deranglem  34904  derangsn  34908  derangenlem  34909  subfacp1lem4  34921  subfacp1lem5  34922  subfacp1lem6  34923  cvmfolem  35017  cvmliftlem6  35028  poimirlem1  37222  poimirlem2  37223  poimirlem3  37224  poimirlem4  37225  poimirlem6  37227  poimirlem7  37228  poimirlem9  37230  poimirlem11  37232  poimirlem12  37233  poimirlem16  37237  poimirlem17  37238  poimirlem19  37240  poimirlem20  37241  poimirlem22  37243  poimirlem26  37247  poimirlem27  37248  poimirlem28  37249  poimirlem32  37253  mblfinlem2  37259  dvasin  37305  f1ocan1fv  37327  metf1o  37356  ismtyval  37401  isismty  37402  ismtyima  37404  ismtyhmeolem  37405  ismtybndlem  37407  ismrer1  37439  reheibor  37440  grposnOLD  37483  rngoisocnv  37582  lflnegl  38675  lautset  39682  islaut  39683  lautcl  39687  lautco  39697  pautsetN  39698  ispautN  39699  ldilco  39716  ltrncoidN  39728  ltrncoval  39745  trlcoabs2N  40322  trlcoat  40323  trlcone  40328  cdlemg47a  40334  cdlemg46  40335  cdlemg47  40336  trljco  40340  tgrpgrplem  40349  tendoidcl  40369  tendo0co2  40388  tendo0pl  40391  cdlemi2  40419  cdlemk2  40432  cdlemk4  40434  cdlemk8  40438  cdlemkid2  40524  cdlemk45  40547  cdlemk53b  40556  cdlemk53  40557  cdlemk55a  40559  erng1r  40595  tendocnv  40621  dvalveclem  40625  dva0g  40627  dvhgrp  40707  dvh0g  40711  dvhopN  40716  cdlemn3  40797  cdlemn8  40804  cdlemn9  40805  dihordlem7b  40815  dihopelvalcpre  40848  dihmeetlem1N  40890  dihglblem5apreN  40891  lcfrlem13  41155  hvmapclN  41364  hvmapcl2  41366  dvrelog2  41664  dvrelog3  41665  sticksstones3  41748  sticksstones17  41763  sticksstones18  41764  sticksstones19  41765  metakunt33  41820  mapfzcons  42275  mzpresrename  42309  diophrw  42318  eldioph2  42321  diophren  42372  kelac1  42626  imasgim  42663  lnrfg  42682  nvocnvb  42991  brco2f1o  43601  brco3f1o  43602  clsneikex  43675  clsneinex  43676  clsneiel1  43677  neicvgmex  43686  neicvgel1  43688  dssmapntrcls  43697  stoweidlem27  45550  stoweidlem31  45554  stoweidlem39  45562  fourierdlem20  45650  fourierdlem50  45679  fourierdlem52  45681  fourierdlem54  45683  fourierdlem64  45693  fourierdlem76  45705  fourierdlem102  45731  fourierdlem114  45743  sge0f1o  45905  nnfoctbdjlem  45978  isomenndlem  46053  ovnsubaddlem1  46093  reuf1odnf  46622  reuf1od  46623  f1oresf1o2  46806  fundcmpsurbijinjpreimafv  46881  fundcmpsurinjimaid  46885  grimfn  47346  isgrim  47349  isuspgrim0lem  47352  isuspgrim0  47353  uspgrimprop  47354  isuspgrim  47356  grimuhgr  47359  grimco  47361  gricushgr  47366  1hegrlfgr  47377  funcringcsetcALTV2lem8  47542  funcringcsetclem8ALTV  47565  itcovalendof  47925  thincciso  48238  amgmwlem  48418