Theorem f1of 6802

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

Syntax hints:   → wi 4  ⟶wf 6509  –1-1→wf1 6510  –1-1-onto→wf1o 6512

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 207  df-an 396  df-f1 6518  df-f1o 6520

This theorem is referenced by:  f1ofn  6803  f1ompt  7085  f1oresrab  7101  fsn  7109  fsnunf  7161  f1ounsn  7249  f1ocnvfv1  7253  f1ocnvfv2  7254  fsnex  7260  f1ocnvdm  7262  fcof1oinvd  7270  fveqf1o  7279  isocnv  7307  isocnv3  7309  isores2  7310  isotr  7313  isofr2  7321  isopolem  7322  isosolem  7324  f1oiso2  7329  weniso  7331  f1ofveu  7383  f1oexrnex  7905  f1oabexg  7920  f1oabexgOLD  7921  wemoiso  7954  mptcnfimad  7967  suppsnop  8159  smoiso  8333  mapsnd  8861  ralxpmap  8871  f1oen2g  8942  en1  8997  enfixsn  9054  mapen  9110  ac6sfi  9237  domunfican  9278  fiint  9283  fiintOLD  9284  mapfienlem1  9362  mapfienlem2  9363  mapfienlem3  9364  mapfien  9365  supisoex  9432  supiso  9433  ordiso2  9474  unxpwdom2  9547  cantnfle  9630  cantnfp1lem3  9639  cantnflem1b  9645  cantnflem1d  9647  cantnflem1  9648  cnfcomlem  9658  cnfcom  9659  cnfcom2lem  9660  cnfcom2  9661  cnfcom3lem  9662  cnfcom3  9663  cnfcom3clem  9664  djuin  9877  infxpenlem  9972  infxpenc  9977  infxpenc2lem2  9979  fseqenlem1  9983  acndom  10010  acndom2  10013  infpwfien  10021  iunfictbso  10073  infmap2  10176  ackbij2lem2  10198  infpssrlem3  10264  infpssrlem4  10265  fin23lem30  10301  isf32lem6  10317  isf32lem7  10318  isf32lem8  10319  enfin1ai  10343  axcc3  10397  axcclem  10416  ttukeylem7  10474  fpwwe2lem5  10594  fpwwe2lem6  10595  fpwwe2lem8  10597  canthp1lem2  10612  canthp1  10613  pwfseqlem4a  10620  pwfseqlem5  10622  axdc4uzlem  13954  seqf1olem1  14012  seqf1olem2  14013  seqf1o  14014  hashkf  14303  hasheqf1oi  14322  hasheqf1od  14324  hashcl  14327  hashgadd  14348  hashfacen  14425  hashf1lem1  14426  fz1isolem  14432  seqcoll  14435  seqcoll2  14436  cnrecnv  15137  sumeq2ii  15665  summolem3  15686  summolem2a  15687  fsum  15692  fsumf1o  15695  fsumss  15697  fsumcl2lem  15703  fsumadd  15712  fsummulc2  15756  fsumrelem  15779  ackbijnn  15800  prodeq2ii  15883  prodmolem3  15905  prodmolem2a  15906  fprod  15913  fprodf1o  15918  fprodss  15920  fprodser  15921  fprodcl2lem  15922  fprodmul  15932  fproddiv  15933  fprodn0  15951  fproddvdsd  16311  sadcaddlem  16433  sadadd2lem  16435  sadadd3  16437  sadaddlem  16442  sadasslem  16446  sadeq  16448  phimullem  16755  eulerthlem1  16757  eulerthlem2  16758  unbenlem  16885  vdwlem8  16965  0ram  16997  wunndx  17171  xpsaddlem  17542  xpsvsca  17546  xpsle  17548  idfucl  17849  setccatid  18052  setcinv  18058  catcisolem  18078  estrccatid  18099  funcestrcsetclem7  18113  funcestrcsetclem8  18114  funcsetcestrclem7  18128  funcsetcestrclem8  18129  yonffthlem  18249  gsumpropd2lem  18612  mgmhmf1o  18633  idmgmhm  18634  idmhm  18728  mhmf1o  18729  gsumws1  18771  ielefmnd  18820  idghm  19169  ghmf1o  19186  symgbas  19308  elsymgbas  19310  symgbasf  19312  symgbasfi  19315  symg1bas  19327  symggrp  19336  lactghmga  19341  symgfixf1  19373  f1omvdmvd  19379  f1omvdconj  19382  f1omvdco2  19384  pmtrfconj  19402  symggen  19406  pmtrdifellem1  19412  pmtrdifellem2  19413  psgnunilem1  19429  gsumval3eu  19840  gsumval3lem1  19841  gsumval3  19843  gsumzf1o  19848  gsumconst  19870  gsumsub  19884  gsumcom2  19911  dprdfsub  19959  dprdf1o  19970  dprdsn  19974  ablfaclem2  20024  rngisomfv1  20380  rngisom1  20381  rngisomring1  20383  fidomndrnglem  20687  srngcl  20764  lmhmf1o  20959  gsumfsum  21357  zntoslem  21472  islinds2  21728  lindsmm  21743  psrass1lem  21847  psrnegcl  21869  psrlinv  21870  coe1f2  22100  coe1add  22156  evls1rhmlem  22214  evl1sca  22227  pf1ind  22248  mat1dimelbas  22364  mat1f  22375  mdetleib2  22481  mdetrsca  22496  mdetralt  22501  mdetunilem7  22511  mdetunilem9  22513  ssidcn  23148  hmphdis  23689  indishmph  23691  cmphaushmeo  23693  ordthmeolem  23694  txhmeo  23696  qtopf1  23709  ufldom  23855  symgtgp  23999  tsmsf1o  24038  iducn  24176  imasdsf1olem  24267  xpsdsval  24275  imasf1obl  24382  icchmeo  24844  icchmeoOLD  24845  iccpnfcnv  24848  xrhmeo  24850  cnheiborlem  24859  ovolctb  25397  ovoliunlem1  25409  ovoliunlem2  25410  iunmbl2  25464  dyadmbl  25507  vitalilem2  25516  vitalilem3  25517  vitalilem4  25518  vitalilem5  25519  mbfid  25542  dvid  25825  dvexp  25863  dvcnvlem  25886  dvcnv  25887  dvcnvrelem2  25929  dvcnvre  25930  efcvx  26365  reefgim  26366  efif1olem4  26460  eff1olem  26463  logrncl  26482  relogcl  26490  dvrelog  26552  relogcn  26553  logcn  26562  logf1o2  26565  dvlog  26566  dvlog2  26568  advlog  26569  advlogexp  26570  logtayl  26575  logccv  26578  dvcxp1  26655  loglesqrt  26677  asinrebnd  26817  dvatan  26851  efrlim  26885  efrlimOLD  26886  amgmlem  26906  lgamcvg2  26971  wilthlem2  26985  wilthlem3  26986  sqff1o  27098  lgsqrlem4  27266  logdivsum  27450  log2sumbnd  27461  isismt  28467  motcl  28472  motco  28473  cnvmot  28474  motgrp  28476  motcgrg  28477  f1otrg  28804  f1otrge  28805  axlowdimlem10  28884  axcontlem5  28901  axcontlem10  28906  uspgriedgedg  29109  upgrres1  29246  umgrres1  29247  upgriseupth  30142  pliguhgr  30421  dmadjrn  31830  unopnorm  31852  unopadj  31854  unoplin  31855  counop  31856  idcnop  31916  idhmop  31917  unopbd  31950  bracnln  32044  cnvbraval  32045  leopnmid  32073  nmopleid  32074  hmopidmch  32088  hmopidmpj  32089  disjrdx  32526  fmptco1f1o  32563  isoun  32631  padct  32649  fcobij  32651  fcobijfs  32652  wrdpmcl  32865  ccatws1f1o  32879  ccatws1f1olast  32880  mndlactf1o  32977  mndractf1o  32978  abliso  32983  symgfcoeu  33045  symgcom  33046  pmtrcnel  33052  pmtrcnel2  33053  pmtrcnelor  33054  wrdpmtrlast  33056  cycpmco2f1  33087  cycpmco2rn  33088  cycpmco2lem2  33090  cycpmco2lem3  33091  cycpmco2lem4  33092  cycpmco2lem5  33093  cycpmco2lem6  33094  cycpmco2lem7  33095  cycpmco2  33096  cycpmconjv  33105  cycpmconjslem1  33117  cycpmconjslem2  33118  cycpmconjs  33119  islinds5  33344  ellspds  33345  1arithidomlem1  33512  1arithidomlem2  33513  1arithidom  33514  tpr2rico  33908  xrge0iifmhm  33935  xrge0pluscn  33936  rrhre  34017  esumf1o  34046  volmeas  34227  eulerpartgbij  34369  eulerpartlemmf  34372  eulerpartlemgvv  34373  eulerpartlemgf  34376  eulerpartlemgs2  34377  eulerpartlemn  34378  ballotlemsima  34513  reprpmtf1o  34623  logdivsqrle  34647  hgt750lemg  34651  deranglem  35153  derangsn  35157  derangenlem  35158  subfacp1lem4  35170  subfacp1lem5  35171  subfacp1lem6  35172  cvmfolem  35266  cvmliftlem6  35277  poimirlem1  37610  poimirlem2  37611  poimirlem3  37612  poimirlem4  37613  poimirlem6  37615  poimirlem7  37616  poimirlem9  37618  poimirlem11  37620  poimirlem12  37621  poimirlem16  37625  poimirlem17  37626  poimirlem19  37628  poimirlem20  37629  poimirlem22  37631  poimirlem26  37635  poimirlem27  37636  poimirlem28  37637  poimirlem32  37641  mblfinlem2  37647  dvasin  37693  f1ocan1fv  37715  metf1o  37744  ismtyval  37789  isismty  37790  ismtyima  37792  ismtyhmeolem  37793  ismtybndlem  37795  ismrer1  37827  reheibor  37828  grposnOLD  37871  rngoisocnv  37970  lflnegl  39064  lautset  40071  islaut  40072  lautcl  40076  lautco  40086  pautsetN  40087  ispautN  40088  ldilco  40105  ltrncoidN  40117  ltrncoval  40134  trlcoabs2N  40711  trlcoat  40712  trlcone  40717  cdlemg47a  40723  cdlemg46  40724  cdlemg47  40725  trljco  40729  tgrpgrplem  40738  tendoidcl  40758  tendo0co2  40777  tendo0pl  40780  cdlemi2  40808  cdlemk2  40821  cdlemk4  40823  cdlemk8  40827  cdlemkid2  40913  cdlemk45  40936  cdlemk53b  40945  cdlemk53  40946  cdlemk55a  40948  erng1r  40984  tendocnv  41010  dvalveclem  41014  dva0g  41016  dvhgrp  41096  dvh0g  41100  dvhopN  41105  cdlemn3  41186  cdlemn8  41193  cdlemn9  41194  dihordlem7b  41204  dihopelvalcpre  41237  dihmeetlem1N  41279  dihglblem5apreN  41280  lcfrlem13  41544  hvmapclN  41753  hvmapcl2  41755  dvrelog2  42047  dvrelog3  42048  sticksstones3  42131  sticksstones17  42146  sticksstones18  42147  sticksstones19  42148  readvrec2  42344  readvrec  42345  mapfzcons  42697  mzpresrename  42731  diophrw  42740  eldioph2  42743  diophren  42794  kelac1  43045  imasgim  43082  lnrfg  43101  nvocnvb  43404  brco2f1o  44014  brco3f1o  44015  clsneikex  44088  clsneinex  44089  clsneiel1  44090  neicvgmex  44099  neicvgel1  44101  dssmapntrcls  44110  stoweidlem27  46018  stoweidlem31  46022  stoweidlem39  46030  fourierdlem20  46118  fourierdlem50  46147  fourierdlem52  46149  fourierdlem54  46151  fourierdlem64  46161  fourierdlem76  46173  fourierdlem102  46199  fourierdlem114  46211  sge0f1o  46373  nnfoctbdjlem  46446  isomenndlem  46521  ovnsubaddlem1  46561  3f1oss1  47066  reuf1odnf  47098  reuf1od  47099  f1oresf1o2  47282  fundcmpsurbijinjpreimafv  47398  fundcmpsurinjimaid  47402  grimfn  47869  isgrim  47872  grimuhgr  47877  grimco  47879  uhgrimedgi  47880  isuspgrim0lem  47883  isuspgrim0  47884  isuspgrim  47886  upgrimwlklem4  47890  gricushgr  47907  isubgrgrim  47919  uhgrimisgrgriclem  47920  uhgrimisgrgric  47921  clnbgrgrim  47924  grimedg  47925  grtriclwlk3  47934  isubgr3stgrlem3  47957  isubgr3stgrlem4  47958  isubgr3stgrlem6  47960  isubgr3stgrlem7  47961  isubgr3stgrlem8  47962  isubgr3stgrlem9  47963  grlimfn  47968  isgrlim  47971  uspgrlimlem1  47977  uspgrlimlem2  47978  uspgrlimlem3  47979  uspgrlimlem4  47980  grlimgrtrilem2  47984  grlictr  47997  clnbgr3stgrgrlic  48001  1hegrlfgr  48110  funcringcsetcALTV2lem8  48275  funcringcsetclem8ALTV  48298  itcovalendof  48648  uptrlem1  49183  swapf2f1oaALT  49249  swapfcoa  49252  swapffunc  49253  fucoppc  49379  thincciso  49422  thinccisod  49423  amgmwlem  49768