Theorem f1of 6050

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

Syntax hints:   → wi 4  ⟶wf 5800  –1-1→wf1 5801  –1-1-onto→wf1o 5803

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 196  df-an 385  df-f1 5809  df-f1o 5811

This theorem is referenced by:  f1ofn  6051  f1ompt  6290  f1oresrab  6302  fsn  6308  fsnunf  6356  f1ocnvfv1  6432  f1ocnvfv2  6433  fsnex  6438  f1ocnvdm  6440  fcof1oinvd  6448  fveqf1o  6457  isocnv  6480  isocnv3  6482  isores2  6483  isotr  6486  isofr2  6494  isopolem  6495  isosolem  6497  f1oiso2  6502  weniso  6504  f1ofveu  6544  f1oexrnex  7008  f1oabexg  7018  wemoiso  7044  suppsnop  7196  smoiso  7346  mapsn  7785  ralxpmap  7793  f1oen2g  7858  en1  7909  enfixsn  7954  mapen  8009  ac6sfi  8089  domunfican  8118  fiint  8122  mapfienlem1  8193  mapfienlem2  8194  mapfienlem3  8195  mapfien  8196  supisoex  8263  supiso  8264  ordiso2  8303  ordtypelem10  8315  hartogslem1  8330  unxpwdom2  8376  cantnfle  8451  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1d  8468  cantnflem1  8469  cnfcomlem  8479  cnfcom  8480  cnfcom2lem  8481  cnfcom2  8482  cnfcom3lem  8483  cnfcom3  8484  cnfcom3clem  8485  infxpenlem  8719  infxpenc  8724  infxpenc2lem2  8726  fseqenlem1  8730  acndom  8757  acndom2  8760  infpwfien  8768  iunfictbso  8820  infmap2  8923  ackbij2lem2  8945  infpssrlem3  9010  infpssrlem4  9011  fin23lem30  9047  isf32lem6  9063  isf32lem7  9064  isf32lem8  9065  enfin1ai  9089  axcc3  9143  axcclem  9162  ttukeylem7  9220  fpwwe2lem6  9336  fpwwe2lem7  9337  fpwwe2lem9  9339  canthp1lem2  9354  canthp1  9355  pwfseqlem4a  9362  pwfseqlem5  9364  dfle2  11856  axdc4uzlem  12644  seqf1olem1  12702  seqf1olem2  12703  seqf1o  12704  hashkf  12981  hasheqf1oi  13002  hasheqf1oiOLD  13003  hasheqf1od  13006  hashcl  13009  hashgadd  13027  hashfacen  13095  hashf1lem1  13096  fz1isolem  13102  seqcoll  13105  seqcoll2  13106  cnrecnv  13753  sumeq2ii  14271  summolem3  14292  summolem2a  14293  fsum  14298  fsumf1o  14301  fsumss  14303  fsumcl2lem  14309  fsumadd  14317  fsummulc2  14358  fsumrelem  14380  ackbijnn  14399  prodeq2ii  14482  prodmolem3  14502  prodmolem2a  14503  fprod  14510  fprodf1o  14515  fprodss  14517  fprodser  14518  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodn0  14548  fproddvdsd  14897  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  sadaddlem  15026  sadasslem  15030  sadeq  15032  phimullem  15322  eulerthlem1  15324  eulerthlem2  15325  unbenlem  15450  vdwlem8  15530  0ram  15562  wunndx  15711  xpsaddlem  16058  xpsvsca  16062  xpsle  16064  idfucl  16364  setccatid  16557  setcinv  16563  catcisolem  16579  estrccatid  16595  funcestrcsetclem7  16609  funcestrcsetclem8  16610  funcsetcestrclem7  16624  funcsetcestrclem8  16625  yonffthlem  16745  gsumpropd2lem  17096  idmhm  17167  mhmf1o  17168  gsumws1  17199  idghm  17498  ghmf1o  17513  symgval  17622  symgbas  17623  elsymgbas  17625  symgbasf  17627  symgbasfi  17629  symg1bas  17639  symggrp  17643  symgid  17644  lactghmga  17647  symgfixf1  17680  f1omvdmvd  17686  f1omvdconj  17689  f1omvdco2  17691  pmtrfconj  17709  symggen  17713  pmtrdifellem1  17719  pmtrdifellem2  17720  psgnunilem1  17736  gsumval3eu  18128  gsumval3lem1  18129  gsumval3  18131  gsumzf1o  18136  gsumconst  18157  gsumsub  18171  gsumcom2  18197  dprdfsub  18243  dprdf1o  18254  dprdsn  18258  ablfaclem2  18308  srngcl  18678  lmhmf1o  18867  fidomndrnglem  19127  psrass1lem  19198  psrnegcl  19217  psrlinv  19218  coe1f2  19400  coe1add  19455  evls1rhmlem  19507  evl1sca  19519  pf1ind  19540  gsumfsum  19632  zntoslem  19724  islinds2  19971  lindsmm  19986  mat1dimelbas  20096  mat1f  20107  mdetleib2  20213  mdetrsca  20228  mdetralt  20233  mdetunilem7  20243  mdetunilem9  20245  ssidcn  20869  hausdiag  21258  hmphdis  21409  indishmph  21411  cmphaushmeo  21413  ordthmeolem  21414  txhmeo  21416  qtopf1  21429  ufldom  21576  symgtgp  21715  tsmsf1o  21758  iducn  21897  imasdsf1olem  21988  xpsdsval  21996  imasf1obl  22103  icchmeo  22548  iccpnfcnv  22551  xrhmeo  22553  cnheiborlem  22561  ovolctb  23065  ovoliunlem1  23077  ovoliunlem2  23078  iunmbl2  23132  dyadmbl  23174  vitalilem2  23184  vitalilem3  23185  vitalilem4  23186  vitalilem5  23187  mbfid  23209  dvid  23487  dvexp  23522  dvcnvlem  23543  dvcnv  23544  dvcnvrelem2  23585  dvcnvre  23586  efcvx  24007  reefgim  24008  efif1olem4  24095  eff1olem  24098  logrncl  24118  relogcl  24126  dvrelog  24183  relogcn  24184  logcn  24193  logf1o2  24196  dvlog  24197  dvlog2  24199  advlog  24200  advlogexp  24201  logtayl  24206  logccv  24209  dvcxp1  24281  loglesqrt  24299  asinrebnd  24428  dvatan  24462  efrlim  24496  amgmlem  24516  lgamcvg2  24581  wilthlem2  24595  wilthlem3  24596  sqff1o  24708  lgsqrlem4  24874  logdivsum  25022  log2sumbnd  25033  isismt  25229  motcl  25234  motco  25235  cnvmot  25236  motgrp  25238  motcgrg  25239  f1otrg  25551  f1otrge  25552  axlowdimlem10  25631  axcontlem5  25648  axcontlem10  25653  umgra1  25855  iseupa  26492  eupatrl  26495  eupa0  26501  eupares  26502  eupap1  26503  eupath2lem3  26506  dmadjrn  28138  unopnorm  28160  unopadj  28162  unoplin  28163  counop  28164  idcnop  28224  idhmop  28225  unopbd  28258  bracnln  28352  cnvbraval  28353  leopnmid  28381  nmopleid  28382  hmopidmch  28396  hmopidmpj  28397  disjrdx  28786  isoun  28862  padct  28885  fcobij  28888  fcobijfs  28889  abliso  29027  symgfcoeu  29176  tpr2rico  29286  xrge0iifmhm  29313  xrge0pluscn  29314  rrhre  29393  esumf1o  29439  volmeas  29621  eulerpartgbij  29761  eulerpartlemmf  29764  eulerpartlemgvv  29765  eulerpartlemgf  29768  eulerpartlemgs2  29769  eulerpartlemn  29770  ballotlemsima  29904  deranglem  30402  derangsn  30406  derangenlem  30407  subfacp1lem4  30419  subfacp1lem5  30420  subfacp1lem6  30421  cvmfolem  30515  cvmliftlem6  30526  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem9  32588  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem32  32611  mblfinlem2  32617  dvasin  32666  f1ocan1fv  32691  metf1o  32721  ismtyval  32769  isismty  32770  ismtyima  32772  ismtyhmeolem  32773  ismtybndlem  32775  ismrer1  32807  reheibor  32808  grposnOLD  32851  rngoisocnv  32950  lflnegl  33381  lautset  34386  islaut  34387  lautcl  34391  lautco  34401  pautsetN  34402  ispautN  34403  ldilco  34420  ltrncoidN  34432  ltrncoval  34449  trlcoabs2N  35028  trlcoat  35029  trlcone  35034  cdlemg47a  35040  cdlemg46  35041  cdlemg47  35042  trljco  35046  tgrpgrplem  35055  tendoidcl  35075  tendo0co2  35094  tendo0pl  35097  cdlemi2  35125  cdlemk2  35138  cdlemk4  35140  cdlemk8  35144  cdlemkid2  35230  cdlemk45  35253  cdlemk53b  35262  cdlemk53  35263  cdlemk55a  35265  erng1r  35301  tendocnv  35328  dvalveclem  35332  dva0g  35334  dvhgrp  35414  dvh0g  35418  dvhopN  35423  cdlemn3  35504  cdlemn8  35511  cdlemn9  35512  dihordlem7b  35522  dihopelvalcpre  35555  dihmeetlem1N  35597  dihglblem5apreN  35598  lcfrlem13  35862  hvmapclN  36071  hvmapcl2  36073  mapfzcons  36297  mzpresrename  36331  diophrw  36340  eldioph2  36343  diophren  36395  kelac1  36651  imasgim  36688  lnrfg  36708  brco2f1o  37350  brco3f1o  37351  clsneikex  37424  clsneinex  37425  clsneiel1  37426  neicvgmex  37435  neicvgel1  37437  dssmapntrcls  37446  mapsnd  38383  stoweidlem27  38920  stoweidlem31  38924  stoweidlem39  38932  fourierdlem20  39020  fourierdlem50  39049  fourierdlem52  39051  fourierdlem54  39053  fourierdlem64  39063  fourierdlem76  39075  fourierdlem102  39101  fourierdlem114  39113  sge0f1o  39275  nnfoctbdjlem  39348  isomenndlem  39420  ovnsubaddlem1  39460  upgrres1  40532  umgrres1  40533  1hegrlfgr  40722  upgriseupth  41375  mgmhmf1o  41577  idmgmhm  41578  funcringcsetcALTV2lem8  41835  funcringcsetclem8ALTV  41858  amgmwlem  42357