Theorem f1of 6768

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

Syntax hints:   → wi 4  ⟶wf 6482  –1-1→wf1 6483  –1-1-onto→wf1o 6485

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 6491  df-f1o 6493

This theorem is referenced by:  f1ofn  6769  f1ompt  7049  f1oresrab  7065  fsn  7073  fsnunf  7125  f1ounsn  7213  f1ocnvfv1  7217  f1ocnvfv2  7218  fsnex  7224  f1ocnvdm  7226  fcof1oinvd  7234  fveqf1o  7243  isocnv  7271  isocnv3  7273  isores2  7274  isotr  7277  isofr2  7285  isopolem  7286  isosolem  7288  f1oiso2  7293  weniso  7295  f1ofveu  7347  f1oexrnex  7867  f1oabexg  7882  f1oabexgOLD  7883  wemoiso  7915  mptcnfimad  7928  suppsnop  8118  smoiso  8292  mapsnd  8820  ralxpmap  8830  f1oen2g  8901  en1  8956  enfixsn  9010  mapen  9065  ac6sfi  9189  domunfican  9230  fiint  9235  fiintOLD  9236  mapfienlem1  9314  mapfienlem2  9315  mapfienlem3  9316  mapfien  9317  supisoex  9384  supiso  9385  ordiso2  9426  unxpwdom2  9499  cantnfle  9586  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1d  9603  cantnflem1  9604  cnfcomlem  9614  cnfcom  9615  cnfcom2lem  9616  cnfcom2  9617  cnfcom3lem  9618  cnfcom3  9619  cnfcom3clem  9620  djuin  9833  infxpenlem  9926  infxpenc  9931  infxpenc2lem2  9933  fseqenlem1  9937  acndom  9964  acndom2  9967  infpwfien  9975  iunfictbso  10027  infmap2  10130  ackbij2lem2  10152  infpssrlem3  10218  infpssrlem4  10219  fin23lem30  10255  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  enfin1ai  10297  axcc3  10351  axcclem  10370  ttukeylem7  10428  fpwwe2lem5  10548  fpwwe2lem6  10549  fpwwe2lem8  10551  canthp1lem2  10566  canthp1  10567  pwfseqlem4a  10574  pwfseqlem5  10576  axdc4uzlem  13908  seqf1olem1  13966  seqf1olem2  13967  seqf1o  13968  hashkf  14257  hasheqf1oi  14276  hasheqf1od  14278  hashcl  14281  hashgadd  14302  hashfacen  14379  hashf1lem1  14380  fz1isolem  14386  seqcoll  14389  seqcoll2  14390  cnrecnv  15090  sumeq2ii  15618  summolem3  15639  summolem2a  15640  fsum  15645  fsumf1o  15648  fsumss  15650  fsumcl2lem  15656  fsumadd  15665  fsummulc2  15709  fsumrelem  15732  ackbijnn  15753  prodeq2ii  15836  prodmolem3  15858  prodmolem2a  15859  fprod  15866  fprodf1o  15871  fprodss  15873  fprodser  15874  fprodcl2lem  15875  fprodmul  15885  fproddiv  15886  fprodn0  15904  fproddvdsd  16264  sadcaddlem  16386  sadadd2lem  16388  sadadd3  16390  sadaddlem  16395  sadasslem  16399  sadeq  16401  phimullem  16708  eulerthlem1  16710  eulerthlem2  16711  unbenlem  16838  vdwlem8  16918  0ram  16950  wunndx  17124  xpsaddlem  17495  xpsvsca  17499  xpsle  17501  idfucl  17806  setccatid  18009  setcinv  18015  catcisolem  18035  estrccatid  18056  funcestrcsetclem7  18070  funcestrcsetclem8  18071  funcsetcestrclem7  18085  funcsetcestrclem8  18086  yonffthlem  18206  gsumpropd2lem  18571  mgmhmf1o  18592  idmgmhm  18593  idmhm  18687  mhmf1o  18688  gsumws1  18730  ielefmnd  18779  idghm  19128  ghmf1o  19145  symgbas  19269  elsymgbas  19271  symgbasf  19273  symgbasfi  19276  symg1bas  19288  symggrp  19297  lactghmga  19302  symgfixf1  19334  f1omvdmvd  19340  f1omvdconj  19343  f1omvdco2  19345  pmtrfconj  19363  symggen  19367  pmtrdifellem1  19373  pmtrdifellem2  19374  psgnunilem1  19390  gsumval3eu  19801  gsumval3lem1  19802  gsumval3  19804  gsumzf1o  19809  gsumconst  19831  gsumsub  19845  gsumcom2  19872  dprdfsub  19920  dprdf1o  19931  dprdsn  19935  ablfaclem2  19985  rngisomfv1  20368  rngisom1  20369  rngisomring1  20371  fidomndrnglem  20675  srngcl  20752  lmhmf1o  20968  gsumfsum  21359  zntoslem  21481  islinds2  21738  lindsmm  21753  psrass1lem  21857  psrnegcl  21879  psrlinv  21880  coe1f2  22110  coe1add  22166  evls1rhmlem  22224  evl1sca  22237  pf1ind  22258  mat1dimelbas  22374  mat1f  22385  mdetleib2  22491  mdetrsca  22506  mdetralt  22511  mdetunilem7  22521  mdetunilem9  22523  ssidcn  23158  hmphdis  23699  indishmph  23701  cmphaushmeo  23703  ordthmeolem  23704  txhmeo  23706  qtopf1  23719  ufldom  23865  symgtgp  24009  tsmsf1o  24048  iducn  24186  imasdsf1olem  24277  xpsdsval  24285  imasf1obl  24392  icchmeo  24854  icchmeoOLD  24855  iccpnfcnv  24858  xrhmeo  24860  cnheiborlem  24869  ovolctb  25407  ovoliunlem1  25419  ovoliunlem2  25420  iunmbl2  25474  dyadmbl  25517  vitalilem2  25526  vitalilem3  25527  vitalilem4  25528  vitalilem5  25529  mbfid  25552  dvid  25835  dvexp  25873  dvcnvlem  25896  dvcnv  25897  dvcnvrelem2  25939  dvcnvre  25940  efcvx  26375  reefgim  26376  efif1olem4  26470  eff1olem  26473  logrncl  26492  relogcl  26500  dvrelog  26562  relogcn  26563  logcn  26572  logf1o2  26575  dvlog  26576  dvlog2  26578  advlog  26579  advlogexp  26580  logtayl  26585  logccv  26588  dvcxp1  26665  loglesqrt  26687  asinrebnd  26827  dvatan  26861  efrlim  26895  efrlimOLD  26896  amgmlem  26916  lgamcvg2  26981  wilthlem2  26995  wilthlem3  26996  sqff1o  27108  lgsqrlem4  27276  logdivsum  27460  log2sumbnd  27471  isismt  28497  motcl  28502  motco  28503  cnvmot  28504  motgrp  28506  motcgrg  28507  f1otrg  28834  f1otrge  28835  axlowdimlem10  28914  axcontlem5  28931  axcontlem10  28936  uspgriedgedg  29139  upgrres1  29276  umgrres1  29277  upgriseupth  30169  pliguhgr  30448  dmadjrn  31857  unopnorm  31879  unopadj  31881  unoplin  31882  counop  31883  idcnop  31943  idhmop  31944  unopbd  31977  bracnln  32071  cnvbraval  32072  leopnmid  32100  nmopleid  32101  hmopidmch  32115  hmopidmpj  32116  disjrdx  32553  fmptco1f1o  32590  isoun  32658  padct  32676  fcobij  32678  fcobijfs  32679  wrdpmcl  32892  ccatws1f1o  32906  ccatws1f1olast  32907  mndlactf1o  32997  mndractf1o  32998  abliso  33003  symgfcoeu  33037  symgcom  33038  pmtrcnel  33044  pmtrcnel2  33045  pmtrcnelor  33046  wrdpmtrlast  33048  cycpmco2f1  33079  cycpmco2rn  33080  cycpmco2lem2  33082  cycpmco2lem3  33083  cycpmco2lem4  33084  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2lem7  33087  cycpmco2  33088  cycpmconjv  33097  cycpmconjslem1  33109  cycpmconjslem2  33110  cycpmconjs  33111  islinds5  33314  ellspds  33315  1arithidomlem1  33482  1arithidomlem2  33483  1arithidom  33484  tpr2rico  33878  xrge0iifmhm  33905  xrge0pluscn  33906  rrhre  33987  esumf1o  34016  volmeas  34197  eulerpartgbij  34339  eulerpartlemmf  34342  eulerpartlemgvv  34343  eulerpartlemgf  34346  eulerpartlemgs2  34347  eulerpartlemn  34348  ballotlemsima  34483  reprpmtf1o  34593  logdivsqrle  34617  hgt750lemg  34621  vonf1owev  35080  deranglem  35138  derangsn  35142  derangenlem  35143  subfacp1lem4  35155  subfacp1lem5  35156  subfacp1lem6  35157  cvmfolem  35251  cvmliftlem6  35262  poimirlem1  37600  poimirlem2  37601  poimirlem3  37602  poimirlem4  37603  poimirlem6  37605  poimirlem7  37606  poimirlem9  37608  poimirlem11  37610  poimirlem12  37611  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem22  37621  poimirlem26  37625  poimirlem27  37626  poimirlem28  37627  poimirlem32  37631  mblfinlem2  37637  dvasin  37683  f1ocan1fv  37705  metf1o  37734  ismtyval  37779  isismty  37780  ismtyima  37782  ismtyhmeolem  37783  ismtybndlem  37785  ismrer1  37817  reheibor  37818  grposnOLD  37861  rngoisocnv  37960  lflnegl  39054  lautset  40061  islaut  40062  lautcl  40066  lautco  40076  pautsetN  40077  ispautN  40078  ldilco  40095  ltrncoidN  40107  ltrncoval  40124  trlcoabs2N  40701  trlcoat  40702  trlcone  40707  cdlemg47a  40713  cdlemg46  40714  cdlemg47  40715  trljco  40719  tgrpgrplem  40728  tendoidcl  40748  tendo0co2  40767  tendo0pl  40770  cdlemi2  40798  cdlemk2  40811  cdlemk4  40813  cdlemk8  40817  cdlemkid2  40903  cdlemk45  40926  cdlemk53b  40935  cdlemk53  40936  cdlemk55a  40938  erng1r  40974  tendocnv  41000  dvalveclem  41004  dva0g  41006  dvhgrp  41086  dvh0g  41090  dvhopN  41095  cdlemn3  41176  cdlemn8  41183  cdlemn9  41184  dihordlem7b  41194  dihopelvalcpre  41227  dihmeetlem1N  41269  dihglblem5apreN  41270  lcfrlem13  41534  hvmapclN  41743  hvmapcl2  41745  dvrelog2  42037  dvrelog3  42038  sticksstones3  42121  sticksstones17  42136  sticksstones18  42137  sticksstones19  42138  readvrec2  42334  readvrec  42335  mapfzcons  42689  mzpresrename  42723  diophrw  42732  eldioph2  42735  diophren  42786  kelac1  43036  imasgim  43073  lnrfg  43092  nvocnvb  43395  brco2f1o  44005  brco3f1o  44006  clsneikex  44079  clsneinex  44080  clsneiel1  44081  neicvgmex  44090  neicvgel1  44092  dssmapntrcls  44101  stoweidlem27  46009  stoweidlem31  46013  stoweidlem39  46021  fourierdlem20  46109  fourierdlem50  46138  fourierdlem52  46140  fourierdlem54  46142  fourierdlem64  46152  fourierdlem76  46164  fourierdlem102  46190  fourierdlem114  46202  sge0f1o  46364  nnfoctbdjlem  46437  isomenndlem  46512  ovnsubaddlem1  46552  3f1oss1  47060  reuf1odnf  47092  reuf1od  47093  f1oresf1o2  47276  fundcmpsurbijinjpreimafv  47392  fundcmpsurinjimaid  47396  grimfn  47864  isgrim  47867  grimuhgr  47872  grimco  47874  uhgrimedgi  47875  isuspgrim0lem  47878  isuspgrim0  47879  isuspgrim  47881  upgrimwlklem4  47885  gricushgr  47902  isubgrgrim  47914  uhgrimisgrgriclem  47915  uhgrimisgrgric  47916  clnbgrgrim  47919  grimedg  47920  grtriclwlk3  47930  isubgr3stgrlem3  47953  isubgr3stgrlem4  47954  isubgr3stgrlem6  47956  isubgr3stgrlem7  47957  isubgr3stgrlem8  47958  isubgr3stgrlem9  47959  grlimfn  47964  isgrlim  47967  uspgrlimlem1  47973  uspgrlimlem2  47974  uspgrlimlem3  47975  uspgrlimlem4  47976  grlimprclnbgredg  47982  grlimgredgex  47985  grlimgrtrilem2  47987  grlictr  48000  clnbgr3stgrgrlim  48004  clnbgr3stgrgrlic  48005  1hegrlfgr  48117  funcringcsetcALTV2lem8  48282  funcringcsetclem8ALTV  48305  itcovalendof  48655  uptrlem1  49196  uptr2  49207  swapf2f1oaALT  49264  swapfcoa  49267  swapffunc  49268  fucoppc  49396  thincciso  49439  thinccisod  49440  lmdran  49657  cmdlan  49658  amgmwlem  49788