Theorem f1of 6725

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

Syntax hints:   → wi 4  ⟶wf 6433  –1-1→wf1 6434  –1-1-onto→wf1o 6436

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 397  df-f1 6442  df-f1o 6444

This theorem is referenced by:  f1ofn  6726  f1ompt  6994  f1oresrab  7008  fsn  7016  fsnunf  7066  f1ocnvfv1  7157  f1ocnvfv2  7158  fsnex  7164  f1ocnvdm  7166  fcof1oinvd  7174  fveqf1o  7184  isocnv  7210  isocnv3  7212  isores2  7213  isotr  7216  isofr2  7224  isopolem  7225  isosolem  7227  f1oiso2  7232  weniso  7234  f1ofveu  7279  f1oexrnex  7783  f1oabexg  7792  wemoiso  7825  suppsnop  8003  smoiso  8202  mapsnd  8683  ralxpmap  8693  f1oen2g  8765  en1  8820  en1OLD  8821  enfixsn  8877  mapen  8937  ac6sfi  9067  domunfican  9096  fiint  9100  mapfienlem1  9173  mapfienlem2  9174  mapfienlem3  9175  mapfien  9176  supisoex  9242  supiso  9243  ordiso2  9283  unxpwdom2  9356  cantnfle  9438  cantnfp1lem3  9447  cantnflem1b  9453  cantnflem1d  9455  cantnflem1  9456  cnfcomlem  9466  cnfcom  9467  cnfcom2lem  9468  cnfcom2  9469  cnfcom3lem  9470  cnfcom3  9471  cnfcom3clem  9472  djuin  9685  infxpenlem  9778  infxpenc  9783  infxpenc2lem2  9785  fseqenlem1  9789  acndom  9816  acndom2  9819  infpwfien  9827  iunfictbso  9879  infmap2  9983  ackbij2lem2  10005  infpssrlem3  10070  infpssrlem4  10071  fin23lem30  10107  isf32lem6  10123  isf32lem7  10124  isf32lem8  10125  enfin1ai  10149  axcc3  10203  axcclem  10222  ttukeylem7  10280  fpwwe2lem5  10400  fpwwe2lem6  10401  fpwwe2lem8  10403  canthp1lem2  10418  canthp1  10419  pwfseqlem4a  10426  pwfseqlem5  10428  axdc4uzlem  13712  seqf1olem1  13771  seqf1olem2  13772  seqf1o  13773  hashkf  14055  hasheqf1oi  14075  hasheqf1od  14077  hashcl  14080  hashgadd  14101  hashfacen  14175  hashfacenOLD  14176  hashf1lem1  14177  hashf1lem1OLD  14178  fz1isolem  14184  seqcoll  14187  seqcoll2  14188  cnrecnv  14885  sumeq2ii  15414  summolem3  15435  summolem2a  15436  fsum  15441  fsumf1o  15444  fsumss  15446  fsumcl2lem  15452  fsumadd  15461  fsummulc2  15505  fsumrelem  15528  ackbijnn  15549  prodeq2ii  15632  prodmolem3  15652  prodmolem2a  15653  fprod  15660  fprodf1o  15665  fprodss  15667  fprodser  15668  fprodcl2lem  15669  fprodmul  15679  fproddiv  15680  fprodn0  15698  fproddvdsd  16053  sadcaddlem  16173  sadadd2lem  16175  sadadd3  16177  sadaddlem  16182  sadasslem  16186  sadeq  16188  phimullem  16489  eulerthlem1  16491  eulerthlem2  16492  unbenlem  16618  vdwlem8  16698  0ram  16730  wunndx  16905  xpsaddlem  17293  xpsvsca  17297  xpsle  17299  idfucl  17605  setccatid  17808  setcinv  17814  catcisolem  17834  estrccatid  17857  funcestrcsetclem7  17872  funcestrcsetclem8  17873  funcsetcestrclem7  17887  funcsetcestrclem8  17888  yonffthlem  18009  gsumpropd2lem  18372  idmhm  18448  mhmf1o  18449  gsumws1  18485  ielefmnd  18535  idghm  18858  ghmf1o  18873  permsetexOLD  18986  symgbas  18987  elsymgbas  18990  symgbasf  18992  symgbasfi  18995  symg1bas  19007  symggrp  19017  lactghmga  19022  symgfixf1  19054  f1omvdmvd  19060  f1omvdconj  19063  f1omvdco2  19065  pmtrfconj  19083  symggen  19087  pmtrdifellem1  19093  pmtrdifellem2  19094  psgnunilem1  19110  gsumval3eu  19514  gsumval3lem1  19515  gsumval3  19517  gsumzf1o  19522  gsumconst  19544  gsumsub  19558  gsumcom2  19585  dprdfsub  19633  dprdf1o  19644  dprdsn  19648  ablfaclem2  19698  srngcl  20124  lmhmf1o  20317  fidomndrnglem  20587  gsumfsum  20674  zntoslem  20773  islinds2  21029  lindsmm  21044  psrass1lemOLD  21152  psrass1lem  21155  psrnegcl  21174  psrlinv  21175  coe1f2  21389  coe1add  21444  evls1rhmlem  21496  evl1sca  21509  pf1ind  21530  mat1dimelbas  21629  mat1f  21640  mdetleib2  21746  mdetrsca  21761  mdetralt  21766  mdetunilem7  21776  mdetunilem9  21778  ssidcn  22415  hmphdis  22956  indishmph  22958  cmphaushmeo  22960  ordthmeolem  22961  txhmeo  22963  qtopf1  22976  ufldom  23122  symgtgp  23266  tsmsf1o  23305  iducn  23444  imasdsf1olem  23535  xpsdsval  23543  imasf1obl  23653  icchmeo  24113  iccpnfcnv  24116  xrhmeo  24118  cnheiborlem  24126  ovolctb  24663  ovoliunlem1  24675  ovoliunlem2  24676  iunmbl2  24730  dyadmbl  24773  vitalilem2  24782  vitalilem3  24783  vitalilem4  24784  vitalilem5  24785  mbfid  24808  dvid  25091  dvexp  25126  dvcnvlem  25149  dvcnv  25150  dvcnvrelem2  25191  dvcnvre  25192  efcvx  25617  reefgim  25618  efif1olem4  25710  eff1olem  25713  logrncl  25732  relogcl  25740  dvrelog  25801  relogcn  25802  logcn  25811  logf1o2  25814  dvlog  25815  dvlog2  25817  advlog  25818  advlogexp  25819  logtayl  25824  logccv  25827  dvcxp1  25902  loglesqrt  25920  asinrebnd  26060  dvatan  26094  efrlim  26128  amgmlem  26148  lgamcvg2  26213  wilthlem2  26227  wilthlem3  26228  sqff1o  26340  lgsqrlem4  26506  logdivsum  26690  log2sumbnd  26701  isismt  26904  motcl  26909  motco  26910  cnvmot  26911  motgrp  26913  motcgrg  26914  f1otrg  27241  f1otrge  27242  axlowdimlem10  27328  axcontlem5  27345  axcontlem10  27350  upgrres1  27689  umgrres1  27690  upgriseupth  28580  pliguhgr  28857  dmadjrn  30266  unopnorm  30288  unopadj  30290  unoplin  30291  counop  30292  idcnop  30352  idhmop  30353  unopbd  30386  bracnln  30480  cnvbraval  30481  leopnmid  30509  nmopleid  30510  hmopidmch  30524  hmopidmpj  30525  disjrdx  30939  fmptco1f1o  30977  isoun  31043  padct  31063  fcobij  31066  fcobijfs  31067  abliso  31314  symgfcoeu  31360  symgcom  31361  pmtrcnel  31367  pmtrcnel2  31368  pmtrcnelor  31369  cycpmco2f1  31400  cycpmco2rn  31401  cycpmco2lem2  31403  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmco2  31409  cycpmconjv  31418  cycpmconjslem1  31430  cycpmconjslem2  31431  cycpmconjs  31432  islinds5  31572  ellspds  31573  tpr2rico  31871  xrge0iifmhm  31898  xrge0pluscn  31899  rrhre  31980  esumf1o  32027  volmeas  32208  eulerpartgbij  32348  eulerpartlemmf  32351  eulerpartlemgvv  32352  eulerpartlemgf  32355  eulerpartlemgs2  32356  eulerpartlemn  32357  ballotlemsima  32491  reprpmtf1o  32615  logdivsqrle  32639  hgt750lemg  32643  deranglem  33137  derangsn  33141  derangenlem  33142  subfacp1lem4  33154  subfacp1lem5  33155  subfacp1lem6  33156  cvmfolem  33250  cvmliftlem6  33261  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem9  35795  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem32  35818  mblfinlem2  35824  dvasin  35870  f1ocan1fv  35893  metf1o  35922  ismtyval  35967  isismty  35968  ismtyima  35970  ismtyhmeolem  35971  ismtybndlem  35973  ismrer1  36005  reheibor  36006  grposnOLD  36049  rngoisocnv  36148  lflnegl  37097  lautset  38103  islaut  38104  lautcl  38108  lautco  38118  pautsetN  38119  ispautN  38120  ldilco  38137  ltrncoidN  38149  ltrncoval  38166  trlcoabs2N  38743  trlcoat  38744  trlcone  38749  cdlemg47a  38755  cdlemg46  38756  cdlemg47  38757  trljco  38761  tgrpgrplem  38770  tendoidcl  38790  tendo0co2  38809  tendo0pl  38812  cdlemi2  38840  cdlemk2  38853  cdlemk4  38855  cdlemk8  38859  cdlemkid2  38945  cdlemk45  38968  cdlemk53b  38977  cdlemk53  38978  cdlemk55a  38980  erng1r  39016  tendocnv  39042  dvalveclem  39046  dva0g  39048  dvhgrp  39128  dvh0g  39132  dvhopN  39137  cdlemn3  39218  cdlemn8  39225  cdlemn9  39226  dihordlem7b  39236  dihopelvalcpre  39269  dihmeetlem1N  39311  dihglblem5apreN  39312  lcfrlem13  39576  hvmapclN  39785  hvmapcl2  39787  dvrelog2  40079  dvrelog3  40080  sticksstones3  40111  sticksstones17  40126  sticksstones18  40127  sticksstones19  40128  metakunt33  40164  mapfzcons  40545  mzpresrename  40579  diophrw  40588  eldioph2  40591  diophren  40642  kelac1  40895  imasgim  40932  lnrfg  40951  brco2f1o  41649  brco3f1o  41650  clsneikex  41723  clsneinex  41724  clsneiel1  41725  neicvgmex  41734  neicvgel1  41736  dssmapntrcls  41745  stoweidlem27  43575  stoweidlem31  43579  stoweidlem39  43587  fourierdlem20  43675  fourierdlem50  43704  fourierdlem52  43706  fourierdlem54  43708  fourierdlem64  43718  fourierdlem76  43730  fourierdlem102  43756  fourierdlem114  43768  sge0f1o  43927  nnfoctbdjlem  44000  isomenndlem  44075  ovnsubaddlem1  44115  reuf1odnf  44610  reuf1od  44611  f1oresf1o2  44794  fundcmpsurbijinjpreimafv  44870  fundcmpsurinjimaid  44874  isomushgr  45289  isomuspgr  45297  isomgrtrlem  45301  1hegrlfgr  45305  mgmhmf1o  45352  idmgmhm  45353  funcringcsetcALTV2lem8  45612  funcringcsetclem8ALTV  45635  itcovalendof  46026  thincciso  46341  amgmwlem  46517