Theorem f1of 6834

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

Syntax hints:   → wi 4  ⟶wf 6540  –1-1→wf1 6541  –1-1-onto→wf1o 6543

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 398  df-f1 6549  df-f1o 6551

This theorem is referenced by:  f1ofn  6835  f1ompt  7111  f1oresrab  7125  fsn  7133  fsnunf  7183  f1ocnvfv1  7274  f1ocnvfv2  7275  fsnex  7281  f1ocnvdm  7283  fcof1oinvd  7291  fveqf1o  7301  isocnv  7327  isocnv3  7329  isores2  7330  isotr  7333  isofr2  7341  isopolem  7342  isosolem  7344  f1oiso2  7349  weniso  7351  f1ofveu  7403  f1oexrnex  7918  f1oabexg  7927  wemoiso  7960  suppsnop  8163  smoiso  8362  mapsnd  8880  ralxpmap  8890  f1oen2g  8964  en1  9021  en1OLD  9022  enfixsn  9081  mapen  9141  ac6sfi  9287  domunfican  9320  fiint  9324  mapfienlem1  9400  mapfienlem2  9401  mapfienlem3  9402  mapfien  9403  supisoex  9469  supiso  9470  ordiso2  9510  unxpwdom2  9583  cantnfle  9666  cantnfp1lem3  9675  cantnflem1b  9681  cantnflem1d  9683  cantnflem1  9684  cnfcomlem  9694  cnfcom  9695  cnfcom2lem  9696  cnfcom2  9697  cnfcom3lem  9698  cnfcom3  9699  cnfcom3clem  9700  djuin  9913  infxpenlem  10008  infxpenc  10013  infxpenc2lem2  10015  fseqenlem1  10019  acndom  10046  acndom2  10049  infpwfien  10057  iunfictbso  10109  infmap2  10213  ackbij2lem2  10235  infpssrlem3  10300  infpssrlem4  10301  fin23lem30  10337  isf32lem6  10353  isf32lem7  10354  isf32lem8  10355  enfin1ai  10379  axcc3  10433  axcclem  10452  ttukeylem7  10510  fpwwe2lem5  10630  fpwwe2lem6  10631  fpwwe2lem8  10633  canthp1lem2  10648  canthp1  10649  pwfseqlem4a  10656  pwfseqlem5  10658  axdc4uzlem  13948  seqf1olem1  14007  seqf1olem2  14008  seqf1o  14009  hashkf  14292  hasheqf1oi  14311  hasheqf1od  14313  hashcl  14316  hashgadd  14337  hashfacen  14413  hashfacenOLD  14414  hashf1lem1  14415  hashf1lem1OLD  14416  fz1isolem  14422  seqcoll  14425  seqcoll2  14426  cnrecnv  15112  sumeq2ii  15639  summolem3  15660  summolem2a  15661  fsum  15666  fsumf1o  15669  fsumss  15671  fsumcl2lem  15677  fsumadd  15686  fsummulc2  15730  fsumrelem  15753  ackbijnn  15774  prodeq2ii  15857  prodmolem3  15877  prodmolem2a  15878  fprod  15885  fprodf1o  15890  fprodss  15892  fprodser  15893  fprodcl2lem  15894  fprodmul  15904  fproddiv  15905  fprodn0  15923  fproddvdsd  16278  sadcaddlem  16398  sadadd2lem  16400  sadadd3  16402  sadaddlem  16407  sadasslem  16411  sadeq  16413  phimullem  16712  eulerthlem1  16714  eulerthlem2  16715  unbenlem  16841  vdwlem8  16921  0ram  16953  wunndx  17128  xpsaddlem  17519  xpsvsca  17523  xpsle  17525  idfucl  17831  setccatid  18034  setcinv  18040  catcisolem  18060  estrccatid  18083  funcestrcsetclem7  18098  funcestrcsetclem8  18099  funcsetcestrclem7  18113  funcsetcestrclem8  18114  yonffthlem  18235  gsumpropd2lem  18598  idmhm  18681  mhmf1o  18682  gsumws1  18719  ielefmnd  18768  idghm  19107  ghmf1o  19122  permsetexOLD  19237  symgbas  19238  elsymgbas  19241  symgbasf  19243  symgbasfi  19246  symg1bas  19258  symggrp  19268  lactghmga  19273  symgfixf1  19305  f1omvdmvd  19311  f1omvdconj  19314  f1omvdco2  19316  pmtrfconj  19334  symggen  19338  pmtrdifellem1  19344  pmtrdifellem2  19345  psgnunilem1  19361  gsumval3eu  19772  gsumval3lem1  19773  gsumval3  19775  gsumzf1o  19780  gsumconst  19802  gsumsub  19816  gsumcom2  19843  dprdfsub  19891  dprdf1o  19902  dprdsn  19906  ablfaclem2  19956  srngcl  20463  lmhmf1o  20657  fidomndrnglem  20925  gsumfsum  21012  zntoslem  21112  islinds2  21368  lindsmm  21383  psrass1lemOLD  21493  psrass1lem  21496  psrnegcl  21515  psrlinv  21516  coe1f2  21733  coe1add  21786  evls1rhmlem  21840  evl1sca  21853  pf1ind  21874  mat1dimelbas  21973  mat1f  21984  mdetleib2  22090  mdetrsca  22105  mdetralt  22110  mdetunilem7  22120  mdetunilem9  22122  ssidcn  22759  hmphdis  23300  indishmph  23302  cmphaushmeo  23304  ordthmeolem  23305  txhmeo  23307  qtopf1  23320  ufldom  23466  symgtgp  23610  tsmsf1o  23649  iducn  23788  imasdsf1olem  23879  xpsdsval  23887  imasf1obl  23997  icchmeo  24457  iccpnfcnv  24460  xrhmeo  24462  cnheiborlem  24470  ovolctb  25007  ovoliunlem1  25019  ovoliunlem2  25020  iunmbl2  25074  dyadmbl  25117  vitalilem2  25126  vitalilem3  25127  vitalilem4  25128  vitalilem5  25129  mbfid  25152  dvid  25435  dvexp  25470  dvcnvlem  25493  dvcnv  25494  dvcnvrelem2  25535  dvcnvre  25536  efcvx  25961  reefgim  25962  efif1olem4  26054  eff1olem  26057  logrncl  26076  relogcl  26084  dvrelog  26145  relogcn  26146  logcn  26155  logf1o2  26158  dvlog  26159  dvlog2  26161  advlog  26162  advlogexp  26163  logtayl  26168  logccv  26171  dvcxp1  26248  loglesqrt  26266  asinrebnd  26406  dvatan  26440  efrlim  26474  amgmlem  26494  lgamcvg2  26559  wilthlem2  26573  wilthlem3  26574  sqff1o  26686  lgsqrlem4  26852  logdivsum  27036  log2sumbnd  27047  isismt  27785  motcl  27790  motco  27791  cnvmot  27792  motgrp  27794  motcgrg  27795  f1otrg  28122  f1otrge  28123  axlowdimlem10  28209  axcontlem5  28226  axcontlem10  28231  upgrres1  28570  umgrres1  28571  upgriseupth  29460  pliguhgr  29739  dmadjrn  31148  unopnorm  31170  unopadj  31172  unoplin  31173  counop  31174  idcnop  31234  idhmop  31235  unopbd  31268  bracnln  31362  cnvbraval  31363  leopnmid  31391  nmopleid  31392  hmopidmch  31406  hmopidmpj  31407  disjrdx  31822  fmptco1f1o  31857  isoun  31923  padct  31944  fcobij  31947  fcobijfs  31948  abliso  32197  symgfcoeu  32243  symgcom  32244  pmtrcnel  32250  pmtrcnel2  32251  pmtrcnelor  32252  cycpmco2f1  32283  cycpmco2rn  32284  cycpmco2lem2  32286  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmco2  32292  cycpmconjv  32301  cycpmconjslem1  32313  cycpmconjslem2  32314  cycpmconjs  32315  islinds5  32480  ellspds  32481  tpr2rico  32892  xrge0iifmhm  32919  xrge0pluscn  32920  rrhre  33001  esumf1o  33048  volmeas  33229  eulerpartgbij  33371  eulerpartlemmf  33374  eulerpartlemgvv  33375  eulerpartlemgf  33378  eulerpartlemgs2  33379  eulerpartlemn  33380  ballotlemsima  33514  reprpmtf1o  33638  logdivsqrle  33662  hgt750lemg  33666  deranglem  34157  derangsn  34161  derangenlem  34162  subfacp1lem4  34174  subfacp1lem5  34175  subfacp1lem6  34176  cvmfolem  34270  cvmliftlem6  34281  gg-icchmeo  35170  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem9  36497  poimirlem11  36499  poimirlem12  36500  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem32  36520  mblfinlem2  36526  dvasin  36572  f1ocan1fv  36594  metf1o  36623  ismtyval  36668  isismty  36669  ismtyima  36671  ismtyhmeolem  36672  ismtybndlem  36674  ismrer1  36706  reheibor  36707  grposnOLD  36750  rngoisocnv  36849  lflnegl  37946  lautset  38953  islaut  38954  lautcl  38958  lautco  38968  pautsetN  38969  ispautN  38970  ldilco  38987  ltrncoidN  38999  ltrncoval  39016  trlcoabs2N  39593  trlcoat  39594  trlcone  39599  cdlemg47a  39605  cdlemg46  39606  cdlemg47  39607  trljco  39611  tgrpgrplem  39620  tendoidcl  39640  tendo0co2  39659  tendo0pl  39662  cdlemi2  39690  cdlemk2  39703  cdlemk4  39705  cdlemk8  39709  cdlemkid2  39795  cdlemk45  39818  cdlemk53b  39827  cdlemk53  39828  cdlemk55a  39830  erng1r  39866  tendocnv  39892  dvalveclem  39896  dva0g  39898  dvhgrp  39978  dvh0g  39982  dvhopN  39987  cdlemn3  40068  cdlemn8  40075  cdlemn9  40076  dihordlem7b  40086  dihopelvalcpre  40119  dihmeetlem1N  40161  dihglblem5apreN  40162  lcfrlem13  40426  hvmapclN  40635  hvmapcl2  40637  dvrelog2  40929  dvrelog3  40930  sticksstones3  40964  sticksstones17  40979  sticksstones18  40980  sticksstones19  40981  metakunt33  41017  mapfzcons  41454  mzpresrename  41488  diophrw  41497  eldioph2  41500  diophren  41551  kelac1  41805  imasgim  41842  lnrfg  41861  nvocnvb  42173  brco2f1o  42783  brco3f1o  42784  clsneikex  42857  clsneinex  42858  clsneiel1  42859  neicvgmex  42868  neicvgel1  42870  dssmapntrcls  42879  stoweidlem27  44743  stoweidlem31  44747  stoweidlem39  44755  fourierdlem20  44843  fourierdlem50  44872  fourierdlem52  44874  fourierdlem54  44876  fourierdlem64  44886  fourierdlem76  44898  fourierdlem102  44924  fourierdlem114  44936  sge0f1o  45098  nnfoctbdjlem  45171  isomenndlem  45246  ovnsubaddlem1  45286  reuf1odnf  45815  reuf1od  45816  f1oresf1o2  45999  fundcmpsurbijinjpreimafv  46075  fundcmpsurinjimaid  46079  isomushgr  46494  isomuspgr  46502  isomgrtrlem  46506  1hegrlfgr  46510  mgmhmf1o  46557  idmgmhm  46558  rngisomfv1  46717  rngisom1  46718  rngisomring1  46720  funcringcsetcALTV2lem8  46941  funcringcsetclem8ALTV  46964  itcovalendof  47355  thincciso  47669  amgmwlem  47849