Theorem f1of 6821

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

Syntax hints:   → wi 4  ⟶wf 6533  –1-1→wf1 6534  –1-1-onto→wf1o 6536

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 401  df-f1 6542  df-f1o 6544

This theorem is referenced by:  f1ofn  6822  f1ompt  7107  f1oresrab  7124  fsn  7132  fsnunf  7184  f1ounsn  7271  f1ocnvfv1  7275  f1ocnvfv2  7276  fsnex  7282  f1ocnvdm  7284  fcof1oinvd  7292  fveqf1o  7301  isocnv  7329  isocnv3  7331  isores2  7332  isotr  7335  isofr2  7343  isopolem  7344  isosolem  7346  f1oiso2  7351  weniso  7353  f1ofveu  7405  f1oexrnex  7924  f1oabexg  7938  wemoiso  7970  mptcnfimad  7983  suppsnop  8174  smoiso  8349  mapsnd  8884  ralxpmap  8894  f1oen2g  8965  en1  9021  enfixsn  9074  mapen  9129  ac6sfi  9244  domunfican  9281  fiint  9286  mapfienlem1  9365  mapfienlem2  9366  mapfienlem3  9367  mapfien  9368  supisoex  9435  supiso  9436  ordiso2  9477  unxpwdom2  9550  cantnfle  9640  cantnfp1lem3  9649  cantnflem1b  9655  cantnflem1d  9657  cantnflem1  9658  cnfcomlem  9668  cnfcom  9669  cnfcom2lem  9670  cnfcom2  9671  cnfcom3lem  9672  cnfcom3  9673  cnfcom3clem  9674  djuin  9904  infxpenlem  9997  infxpenc  10002  infxpenc2lem2  10004  fseqenlem1  10008  acndom  10035  acndom2  10038  infpwfien  10046  iunfictbso  10098  infmap2  10200  ackbij2lem2  10222  infpssrlem3  10289  infpssrlem4  10290  fin23lem30  10326  isf32lem6  10342  isf32lem7  10343  isf32lem8  10344  enfin1ai  10368  axcc3  10422  axcclem  10441  ttukeylem7  10499  fpwwe2lem5  10620  fpwwe2lem6  10621  fpwwe2lem8  10623  canthp1lem2  10638  canthp1  10639  pwfseqlem4a  10646  pwfseqlem5  10648  axdc4uzlem  14019  seqf1olem1  14077  seqf1olem2  14078  seqf1o  14079  hashkf  14368  hasheqf1oi  14387  hasheqf1od  14389  hashcl  14392  hashgadd  14413  hashfacen  14491  hashf1lem1  14492  fz1isolem  14498  seqcoll  14501  seqcoll2  14502  cnrecnv  15216  sumeq2ii  15744  summolem3  15765  summolem2a  15766  fsum  15771  fsumf1o  15774  fsumss  15776  fsumcl2lem  15782  fsumadd  15791  fsummulc2  15835  fsumrelem  15859  ackbijnn  15882  prodeq2ii  15965  prodmolem3  15987  prodmolem2a  15988  fprod  15995  fprodf1o  16000  fprodss  16002  fprodser  16003  fprodcl2lem  16004  fprodmul  16014  fproddiv  16015  fprodn0  16033  fproddvdsd  16393  sadcaddlem  16515  sadadd2lem  16517  sadadd3  16519  sadaddlem  16524  sadasslem  16528  sadeq  16530  phimullem  16838  eulerthlem1  16840  eulerthlem2  16841  unbenlem  16968  vdwlem8  17048  0ram  17080  wunndx  17255  xpsaddlem  17627  xpsvsca  17631  xpsle  17633  idfucl  17938  setccatid  18141  setcinv  18147  catcisolem  18167  estrccatid  18188  funcestrcsetclem7  18202  funcestrcsetclem8  18203  funcsetcestrclem7  18217  funcsetcestrclem8  18218  yonffthlem  18338  gsumpropd2lem  18737  mgmhmf1o  18758  idmgmhm  18759  idmhm  18853  mhmf1o  18854  gsumws1  18897  ielefmnd  18946  idghm  19301  ghmf1o  19318  symgbas  19442  elsymgbas  19444  symgbasf  19446  symgbasfi  19449  symg1bas  19461  symggrp  19470  lactghmga  19475  symgfixf1  19507  f1omvdmvd  19513  f1omvdconj  19516  f1omvdco2  19518  pmtrfconj  19536  symggen  19540  pmtrdifellem1  19546  pmtrdifellem2  19547  psgnunilem1  19563  gsumval3eu  19974  gsumval3lem1  19975  gsumval3  19977  gsumzf1o  19982  gsumconst  20004  gsumsub  20018  gsumcom2  20045  dprdfsub  20093  dprdf1o  20104  dprdsn  20108  ablfaclem2  20158  rngisomfv1  20547  rngisom1  20548  rngisomring1  20550  fidomndrnglem  20854  srngcl  20930  lmhmf1o  21145  gsumfsum  21553  zntoslem  21675  islinds2  21932  lindsmm  21947  psrass1lem  22052  psrnegcl  22073  psrlinv  22074  coe1f2  22338  coe1add  22394  evls1rhmlem  22450  evl1sca  22463  pf1ind  22484  mat1dimelbas  22597  mat1f  22608  mdetleib2  22714  mdetrsca  22729  mdetralt  22734  mdetunilem7  22744  mdetunilem9  22746  ssidcn  23381  hmphdis  23922  indishmph  23924  cmphaushmeo  23926  ordthmeolem  23927  txhmeo  23929  qtopf1  23942  ufldom  24088  symgtgp  24232  tsmsf1o  24271  iducn  24408  imasdsf1olem  24499  xpsdsval  24507  imasf1obl  24614  icchmeo  25069  iccpnfcnv  25072  xrhmeo  25074  cnheiborlem  25082  ovolctb  25618  ovoliunlem1  25630  ovoliunlem2  25631  iunmbl2  25685  dyadmbl  25728  vitalilem2  25737  vitalilem3  25738  vitalilem4  25739  vitalilem5  25740  mbfid  25763  dvid  26046  dvexp  26081  dvcnvlem  26104  dvcnv  26105  dvcnvrelem2  26146  dvcnvre  26147  efcvx  26578  reefgim  26579  efif1olem4  26676  eff1olem  26679  logrncl  26698  relogcl  26706  dvrelog  26768  relogcn  26769  logcn  26778  logf1o2  26781  dvlog  26782  dvlog2  26784  advlog  26785  advlogexp  26786  logtayl  26791  logccv  26794  dvcxp1  26871  loglesqrt  26892  asinrebnd  27032  dvatan  27066  efrlim  27100  amgmlem  27120  lgamcvg2  27185  wilthlem2  27199  wilthlem3  27200  sqff1o  27312  lgsqrlem4  27479  logdivsum  27663  log2sumbnd  27674  isismt  28769  motcl  28774  motco  28775  cnvmot  28776  motgrp  28778  motcgrg  28779  f1otrg  29161  f1otrge  29162  axlowdimlem10  29242  axcontlem5  29259  axcontlem10  29264  uspgriedgedg  29467  upgrres1  29604  umgrres1  29605  upgriseupth  30499  pliguhgr  30779  dmadjrn  32188  unopnorm  32210  unopadj  32212  unoplin  32213  counop  32214  idcnop  32274  idhmop  32275  unopbd  32308  bracnln  32402  cnvbraval  32403  leopnmid  32431  nmopleid  32432  hmopidmch  32446  hmopidmpj  32447  disjrdx  32877  fmptco1f1o  32919  isoun  32988  padct  33004  fcobij  33006  fcobijfs  33007  fcobijfs2  33008  wrdpmcl  33199  ccatws1f1o  33212  ccatws1f1olast  33213  mndlactf1o  33291  mndractf1o  33292  abliso  33296  symgfcoeu  33343  symgcom  33344  pmtrcnel  33350  pmtrcnel2  33351  pmtrcnelor  33352  wrdpmtrlast  33354  cycpmco2f1  33385  cycpmco2rn  33386  cycpmco2lem2  33388  cycpmco2lem3  33389  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cycpmco2lem7  33393  cycpmco2  33394  cycpmconjv  33403  cycpmconjslem1  33415  cycpmconjslem2  33416  cycpmconjs  33417  islinds5  33625  ellspds  33626  1arithidomlem1  33770  1arithidomlem2  33771  1arithidom  33772  0mplrim  33849  selvply1rhmlemb  33854  mplvrpmlem  33878  mplvrpmfgalem  33879  mplvrpmmhm  33881  mplvrpmrhm  33882  esplyfval0  33899  esplylem  33901  esplympl  33902  esplymhp  33903  esplyfv1  33904  esplyfv  33905  esplysply  33906  esplyfval3  33907  vieta  33915  tpr2rico  34247  xrge0iifmhm  34274  xrge0pluscn  34275  rrhre  34356  esumf1o  34385  volmeas  34566  eulerpartgbij  34707  eulerpartlemmf  34710  eulerpartlemgvv  34711  eulerpartlemgf  34714  eulerpartlemgs2  34715  eulerpartlemn  34716  ballotlemsima  34851  reprpmtf1o  34958  logdivsqrle  34982  hgt750lemg  34986  vonf1owevOLD  35527  deranglem  35591  derangsn  35595  derangenlem  35596  subfacp1lem4  35608  subfacp1lem5  35609  subfacp1lem6  35610  cvmfolem  35704  cvmliftlem6  35715  poimirlem1  38195  poimirlem2  38196  poimirlem3  38197  poimirlem4  38198  poimirlem6  38200  poimirlem7  38201  poimirlem9  38203  poimirlem11  38205  poimirlem12  38206  poimirlem16  38210  poimirlem17  38211  poimirlem19  38213  poimirlem20  38214  poimirlem22  38216  poimirlem26  38220  poimirlem27  38221  poimirlem28  38222  poimirlem32  38226  mblfinlem2  38232  dvasin  38278  f1ocan1fv  38300  metf1o  38329  ismtyval  38374  isismty  38375  ismtyima  38377  ismtyhmeolem  38378  ismtybndlem  38380  ismrer1  38412  reheibor  38413  grposnOLD  38456  rngoisocnv  38555  lflnegl  39775  lautset  40781  islaut  40782  lautcl  40786  lautco  40796  pautsetN  40797  ispautN  40798  ldilco  40815  ltrncoidN  40827  ltrncoval  40844  trlcoabs2N  41421  trlcoat  41422  trlcone  41427  cdlemg47a  41433  cdlemg46  41434  cdlemg47  41435  trljco  41439  tgrpgrplem  41448  tendoidcl  41468  tendo0co2  41487  tendo0pl  41490  cdlemi2  41518  cdlemk2  41531  cdlemk4  41533  cdlemk8  41537  cdlemkid2  41623  cdlemk45  41646  cdlemk53b  41655  cdlemk53  41656  cdlemk55a  41658  erng1r  41694  tendocnv  41720  dvalveclem  41724  dva0g  41726  dvhgrp  41806  dvh0g  41810  dvhopN  41815  cdlemn3  41896  cdlemn8  41903  cdlemn9  41904  dihordlem7b  41914  dihopelvalcpre  41947  dihmeetlem1N  41989  dihglblem5apreN  41990  lcfrlem13  42254  hvmapclN  42463  hvmapcl2  42465  dvrelog2  42756  dvrelog3  42757  sticksstones3  42840  sticksstones17  42855  sticksstones18  42856  sticksstones19  42857  readvrec2  43047  readvrec  43048  mapfzcons  43374  mzpresrename  43408  diophrw  43417  eldioph2  43420  diophren  43467  kelac1  43717  imasgim  43754  lnrfg  43773  nvocnvb  44075  brco2f1o  44685  brco3f1o  44686  clsneikex  44759  clsneinex  44760  clsneiel1  44761  neicvgmex  44770  neicvgel1  44772  dssmapntrcls  44781  stoweidlem27  46668  stoweidlem31  46672  stoweidlem39  46680  fourierdlem20  46768  fourierdlem50  46797  fourierdlem52  46799  fourierdlem54  46801  fourierdlem64  46811  fourierdlem76  46823  fourierdlem102  46849  fourierdlem114  46861  sge0f1o  47023  nnfoctbdjlem  47096  isomenndlem  47171  ovnsubaddlem1  47211  3f1oss1  47736  reuf1odnf  47768  reuf1od  47769  f1oresf1o2  47952  fundcmpsurbijinjpreimafv  48080  fundcmpsurinjimaid  48084  grimfn  48568  isgrim  48571  grimuhgr  48576  grimco  48578  uhgrimedgi  48579  isuspgrim0lem  48582  isuspgrim0  48583  isuspgrim  48585  upgrimwlklem4  48589  gricushgr  48606  isubgrgrim  48618  uhgrimisgrgriclem  48619  uhgrimisgrgric  48620  clnbgrgrim  48623  grimedg  48624  grtriclwlk3  48634  isubgr3stgrlem3  48657  isubgr3stgrlem4  48658  isubgr3stgrlem6  48660  isubgr3stgrlem7  48661  isubgr3stgrlem8  48662  isubgr3stgrlem9  48663  grlimfn  48668  isgrlim  48671  uspgrlimlem1  48677  uspgrlimlem2  48678  uspgrlimlem3  48679  uspgrlimlem4  48680  grlimprclnbgredg  48686  grlimgredgex  48689  grlimgrtrilem2  48691  grlictr  48704  clnbgr3stgrgrlim  48708  clnbgr3stgrgrlic  48709  1hegrlfgr  48821  funcringcsetcALTV2lem8  48986  funcringcsetclem8ALTV  49009  itcovalendof  49369  uptrlem1  49908  uptr2  49919  swapf2f1oaALT  49976  swapfcoa  49979  swapffunc  49980  fucoppc  50108  thincciso  50151  thinccisod  50152  lmdran  50369  cmdlan  50370  amgmwlem  50511