Theorem f1of 6590

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

Syntax hints:   → wi 4  ⟶wf 6320  –1-1→wf1 6321  –1-1-onto→wf1o 6323

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 210  df-an 400  df-f1 6329  df-f1o 6331

This theorem is referenced by:  f1ofn  6591  f1ompt  6852  f1oresrab  6866  fsn  6874  fsnunf  6924  f1ocnvfv1  7011  f1ocnvfv2  7012  fsnex  7017  f1ocnvdm  7019  fcof1oinvd  7027  fveqf1o  7037  isocnv  7062  isocnv3  7064  isores2  7065  isotr  7068  isofr2  7076  isopolem  7077  isosolem  7079  f1oiso2  7084  weniso  7086  f1ofveu  7130  f1oexrnex  7614  f1oabexg  7624  wemoiso  7656  suppsnop  7827  smoiso  7982  mapsnd  8433  ralxpmap  8443  f1oen2g  8509  en1  8559  enfixsn  8609  mapen  8665  ac6sfi  8746  domunfican  8775  fiint  8779  mapfienlem1  8852  mapfienlem2  8853  mapfienlem3  8854  mapfien  8855  supisoex  8922  supiso  8923  ordiso2  8963  ordtypelem10  8975  unxpwdom2  9036  cantnfle  9118  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1d  9135  cantnflem1  9136  cnfcomlem  9146  cnfcom  9147  cnfcom2lem  9148  cnfcom2  9149  cnfcom3lem  9150  cnfcom3  9151  cnfcom3clem  9152  djuin  9331  infxpenlem  9424  infxpenc  9429  infxpenc2lem2  9431  fseqenlem1  9435  acndom  9462  acndom2  9465  infpwfien  9473  iunfictbso  9525  infmap2  9629  ackbij2lem2  9651  infpssrlem3  9716  infpssrlem4  9717  fin23lem30  9753  isf32lem6  9769  isf32lem7  9770  isf32lem8  9771  enfin1ai  9795  axcc3  9849  axcclem  9868  ttukeylem7  9926  fpwwe2lem6  10046  fpwwe2lem7  10047  fpwwe2lem9  10049  canthp1lem2  10064  canthp1  10065  pwfseqlem4a  10072  pwfseqlem5  10074  axdc4uzlem  13346  seqf1olem1  13405  seqf1olem2  13406  seqf1o  13407  hashkf  13688  hasheqf1oi  13708  hasheqf1od  13710  hashcl  13713  hashgadd  13734  hashfacen  13808  hashf1lem1  13809  fz1isolem  13815  seqcoll  13818  seqcoll2  13819  cnrecnv  14516  sumeq2ii  15042  summolem3  15063  summolem2a  15064  fsum  15069  fsumf1o  15072  fsumss  15074  fsumcl2lem  15080  fsumadd  15088  fsummulc2  15131  fsumrelem  15154  ackbijnn  15175  prodeq2ii  15259  prodmolem3  15279  prodmolem2a  15280  fprod  15287  fprodf1o  15292  fprodss  15294  fprodser  15295  fprodcl2lem  15296  fprodmul  15306  fproddiv  15307  fprodn0  15325  fproddvdsd  15676  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  sadasslem  15809  sadeq  15811  phimullem  16106  eulerthlem1  16108  eulerthlem2  16109  unbenlem  16234  vdwlem8  16314  0ram  16346  wunndx  16496  xpsaddlem  16838  xpsvsca  16842  xpsle  16844  idfucl  17143  setccatid  17336  setcinv  17342  catcisolem  17358  estrccatid  17374  funcestrcsetclem7  17388  funcestrcsetclem8  17389  funcsetcestrclem7  17403  funcsetcestrclem8  17404  yonffthlem  17524  gsumpropd2lem  17881  idmhm  17957  mhmf1o  17958  gsumws1  17994  ielefmnd  18044  idghm  18365  ghmf1o  18380  permsetex  18490  symgbas  18491  elsymgbas  18494  symgbasf  18496  symgbasfi  18499  symg1bas  18511  symggrp  18520  lactghmga  18525  symgfixf1  18557  f1omvdmvd  18563  f1omvdconj  18566  f1omvdco2  18568  pmtrfconj  18586  symggen  18590  pmtrdifellem1  18596  pmtrdifellem2  18597  psgnunilem1  18613  gsumval3eu  19017  gsumval3lem1  19018  gsumval3  19020  gsumzf1o  19025  gsumconst  19047  gsumsub  19061  gsumcom2  19088  dprdfsub  19136  dprdf1o  19147  dprdsn  19151  ablfaclem2  19201  srngcl  19619  lmhmf1o  19811  fidomndrnglem  20072  gsumfsum  20158  zntoslem  20248  islinds2  20502  lindsmm  20517  psrass1lem  20615  psrnegcl  20634  psrlinv  20635  coe1f2  20838  coe1add  20893  evls1rhmlem  20945  evl1sca  20958  pf1ind  20979  mat1dimelbas  21076  mat1f  21087  mdetleib2  21193  mdetrsca  21208  mdetralt  21213  mdetunilem7  21223  mdetunilem9  21225  ssidcn  21860  hmphdis  22401  indishmph  22403  cmphaushmeo  22405  ordthmeolem  22406  txhmeo  22408  qtopf1  22421  ufldom  22567  symgtgp  22711  tsmsf1o  22750  iducn  22889  imasdsf1olem  22980  xpsdsval  22988  imasf1obl  23095  icchmeo  23546  iccpnfcnv  23549  xrhmeo  23551  cnheiborlem  23559  ovolctb  24094  ovoliunlem1  24106  ovoliunlem2  24107  iunmbl2  24161  dyadmbl  24204  vitalilem2  24213  vitalilem3  24214  vitalilem4  24215  vitalilem5  24216  mbfid  24239  dvid  24521  dvexp  24556  dvcnvlem  24579  dvcnv  24580  dvcnvrelem2  24621  dvcnvre  24622  efcvx  25044  reefgim  25045  efif1olem4  25137  eff1olem  25140  logrncl  25159  relogcl  25167  dvrelog  25228  relogcn  25229  logcn  25238  logf1o2  25241  dvlog  25242  dvlog2  25244  advlog  25245  advlogexp  25246  logtayl  25251  logccv  25254  dvcxp1  25329  loglesqrt  25347  asinrebnd  25487  dvatan  25521  efrlim  25555  amgmlem  25575  lgamcvg2  25640  wilthlem2  25654  wilthlem3  25655  sqff1o  25767  lgsqrlem4  25933  logdivsum  26117  log2sumbnd  26128  isismt  26328  motcl  26333  motco  26334  cnvmot  26335  motgrp  26337  motcgrg  26338  f1otrg  26665  f1otrge  26666  axlowdimlem10  26745  axcontlem5  26762  axcontlem10  26767  upgrres1  27103  umgrres1  27104  upgriseupth  27992  pliguhgr  28269  dmadjrn  29678  unopnorm  29700  unopadj  29702  unoplin  29703  counop  29704  idcnop  29764  idhmop  29765  unopbd  29798  bracnln  29892  cnvbraval  29893  leopnmid  29921  nmopleid  29922  hmopidmch  29936  hmopidmpj  29937  disjrdx  30354  fmptco1f1o  30392  isoun  30461  padct  30481  fcobij  30484  fcobijfs  30485  abliso  30730  symgfcoeu  30776  symgcom  30777  pmtrcnel  30783  pmtrcnel2  30784  pmtrcnelor  30785  cycpmco2f1  30816  cycpmco2rn  30817  cycpmco2lem2  30819  cycpmco2lem3  30820  cycpmco2lem4  30821  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmco2  30825  cycpmconjv  30834  cycpmconjslem1  30846  cycpmconjslem2  30847  cycpmconjs  30848  islinds5  30983  ellspds  30984  tpr2rico  31265  xrge0iifmhm  31292  xrge0pluscn  31293  rrhre  31372  esumf1o  31419  volmeas  31600  eulerpartgbij  31740  eulerpartlemmf  31743  eulerpartlemgvv  31744  eulerpartlemgf  31747  eulerpartlemgs2  31748  eulerpartlemn  31749  ballotlemsima  31883  reprpmtf1o  32007  logdivsqrle  32031  hgt750lemg  32035  deranglem  32526  derangsn  32530  derangenlem  32531  subfacp1lem4  32543  subfacp1lem5  32544  subfacp1lem6  32545  cvmfolem  32639  cvmliftlem6  32650  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem9  35066  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem22  35079  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem32  35089  mblfinlem2  35095  dvasin  35141  f1ocan1fv  35164  metf1o  35193  ismtyval  35238  isismty  35239  ismtyima  35241  ismtyhmeolem  35242  ismtybndlem  35244  ismrer1  35276  reheibor  35277  grposnOLD  35320  rngoisocnv  35419  lflnegl  36372  lautset  37378  islaut  37379  lautcl  37383  lautco  37393  pautsetN  37394  ispautN  37395  ldilco  37412  ltrncoidN  37424  ltrncoval  37441  trlcoabs2N  38018  trlcoat  38019  trlcone  38024  cdlemg47a  38030  cdlemg46  38031  cdlemg47  38032  trljco  38036  tgrpgrplem  38045  tendoidcl  38065  tendo0co2  38084  tendo0pl  38087  cdlemi2  38115  cdlemk2  38128  cdlemk4  38130  cdlemk8  38134  cdlemkid2  38220  cdlemk45  38243  cdlemk53b  38252  cdlemk53  38253  cdlemk55a  38255  erng1r  38291  tendocnv  38317  dvalveclem  38321  dva0g  38323  dvhgrp  38403  dvh0g  38407  dvhopN  38412  cdlemn3  38493  cdlemn8  38500  cdlemn9  38501  dihordlem7b  38511  dihopelvalcpre  38544  dihmeetlem1N  38586  dihglblem5apreN  38587  lcfrlem13  38851  hvmapclN  39060  hvmapcl2  39062  metakunt33  39382  mapfzcons  39657  mzpresrename  39691  diophrw  39700  eldioph2  39703  diophren  39754  kelac1  40007  imasgim  40044  lnrfg  40063  brco2f1o  40735  brco3f1o  40736  clsneikex  40809  clsneinex  40810  clsneiel1  40811  neicvgmex  40820  neicvgel1  40822  dssmapntrcls  40831  stoweidlem27  42669  stoweidlem31  42673  stoweidlem39  42681  fourierdlem20  42769  fourierdlem50  42798  fourierdlem52  42800  fourierdlem54  42802  fourierdlem64  42812  fourierdlem76  42824  fourierdlem102  42850  fourierdlem114  42862  sge0f1o  43021  nnfoctbdjlem  43094  isomenndlem  43169  ovnsubaddlem1  43209  reuf1odnf  43663  reuf1od  43664  f1oresf1o2  43847  fundcmpsurbijinjpreimafv  43924  fundcmpsurinjimaid  43928  isomushgr  44344  isomuspgr  44352  isomgrtrlem  44356  1hegrlfgr  44360  mgmhmf1o  44407  idmgmhm  44408  funcringcsetcALTV2lem8  44667  funcringcsetclem8ALTV  44690  itcovalendof  45083  amgmwlem  45330