Theorem eqid 2234

Description: Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41.

This law is thought to have originated with Aristotle (Metaphysics, Zeta, 17, 1041 a, 10-20). (Thanks to Stefan Allan and BJ for this information.) (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 14-Oct-2017.)

Assertion

Ref	Expression
eqid	⊢ 𝐴 = 𝐴

Proof of Theorem eqid

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		biid 171	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
2	1	eqriv 2231	1 ⊢ 𝐴 = 𝐴

Syntax hints:   = wceq 1398   ∈ wcel 2205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227

This theorem is referenced by:  eqidd  2235  neirr  2423  sbsbc  3049  sbceqal  3101  dfnul2  3514  snidg  3723  prid1g  3800  tpid1  3808  tpid1g  3809  tpid2  3810  tpid2g  3811  tpid3  3813  dfiin2g  4029  eqbrtrid  4149  eqbrtrrid  4150  breqtrdi  4155  opabbii  4182  mpteq2ia  4201  mpteq2da  4204  sucidg  4542  onsucelsucexmidlem1  4655  regexmidlemm  4659  regexmidlem1  4660  reg2exmidlema  4661  regexmid  4662  reg2exmid  4663  reg3exmid  4707  tfisi  4714  finds1  4729  nn0suc  4731  nndceq0  4745  0elnn  4746  nnregexmid  4748  opelxp  4784  relopabv  4884  relopab  4886  relop  4910  ididg  4913  elrnmpt1s  5012  dfiun3g  5019  dfiin3g  5020  dmmptg  5265  funfn  5387  mpt0  5491  f0  5563  dffn4  5601  f1orn  5629  f1oabexg  5631  f1o00  5656  f1o0  5658  fnbrfvb  5720  fnrnfv  5728  funfvdm  5745  fvmptg  5758  fvmptd  5763  fvmpt2d  5769  fvmptdf  5770  mpteqb  5773  fvmptt  5774  fnmptfvd  5787  funfvop  5795  eldmrexrn  5823  fvmptelcdm  5835  fmpttd  5837  fmpt2d  5844  fmptco  5848  fmptcof  5849  fnasrn  5861  fnasrng  5863  funop  5866  mptexg  5916  eufnfv  5922  idref  5935  f1elima  5952  fliftrel  5971  fliftel  5972  fliftel1  5973  fliftcnv  5974  fliftf  5978  fdmrn  6007  riotabiia  6030  acexmidlem2  6055  acexmidlemv  6056  oprabbii  6116  mpoeq12  6121  ovmpodxf  6187  ovmpodf  6193  ov6g  6200  f1ocnvd  6265  f1opw2  6269  f1o3d  6271  suppssov1  6272  ofvalg  6285  off  6288  offval2  6291  ofrfval2  6292  caofinvl  6301  mptexw  6315  abrexex  6319  abrexexg  6320  offres  6341  ofmres  6342  uchoice  6344  op1steq  6386  reldm  6393  mpoexga  6421  mpoexw  6422  mpoex  6423  fnmpoovd  6424  fmpoco  6425  cnvf1o  6434  f1od2  6444  suppssfvg  6476  tposssxp  6493  brtpos2  6495  tpos0  6518  iunon  6528  tfrfun  6564  tfr2a  6565  tfrlemisucfn  6568  tfri1d  6579  tfr1onlemsucfn  6584  tfr1onlemubacc  6590  tfr1on  6594  tfri1dALT  6595  tfrcllemubacc  6603  tfrex  6612  rdgfun  6617  rdgon  6630  rdg0  6631  frec0g  6641  frecfnom  6645  freccllem  6646  freccl  6647  frecfcllem  6648  frecfcl  6649  frecsuclem  6650  0lt1o  6686  oafnex  6690  omfnex  6695  fnoei  6698  oeiexg  6699  oeiv  6702  oacl  6706  omcl  6707  oeicl  6708  oav2  6709  omv2  6711  eqer  6812  ecelqsg  6835  elqsn0m  6850  qsel  6859  qliftf  6867  ecoptocl  6869  eroprf  6875  ecopovsym  6878  ecopovtrn  6879  ecopovsymg  6881  ecopovtrng  6882  th3qlem2  6885  th3q  6887  mapsncnv  6943  mapsnf1o3  6945  mptelixpg  6982  ixpsnf1o  6984  en2d  7020  en3d  7021  dom2lem  7024  dom2  7027  1domsn  7081  xpcomen  7091  pw2f1odclem  7100  pw2f1odc  7101  xpf1o  7110  mapxpen  7114  fidifsnen  7138  exmidpw2en  7185  isbth  7250  snopfsuppdc  7265  elfir  7273  2omap  7282  2omapen  7283  2omapfi  7284  supsnti  7309  djueq1  7344  djueq2  7345  djuf1olem  7357  inl11  7369  updjud  7386  omp1eom  7399  difinfsn  7404  ctmlemr  7412  ctssdclemn0  7414  ctssdclemr  7416  ctssdc  7417  enumct  7419  infnninf  7428  nnnninf  7430  nnnninfeq  7432  nninfisollemne  7435  nninfisol  7437  ismkvnex  7459  mkvprop  7462  nninfwlporlemd  7476  nninfwlpoimlemginf  7480  exmidonfin  7510  exmidaclem  7528  exmidac  7529  cc3  7598  0npi  7644  indpi  7673  recidnq  7724  addnnnq0  7780  mulnnnq0  7781  genpprecll  7845  genppreclu  7846  caucvgprpr  8043  addsrpr  8076  mulsrpr  8077  0nsr  8080  00sr  8100  caucvgsrlemgt1  8126  opelreal  8158  eqresr  8167  axprecex  8211  nntopi  8225  axpre-suploc  8233  mpomulf  8280  ltxrlt  8355  pncan3  8497  apreim  8894  divcanap2  8971  divcanap3  8989  lble  9238  sup3exmid  9248  nn1gt1  9288  0nn0  9528  pnf0xnn0  9587  0z  9605  decaddm10  9785  decmulnc  9793  10p10e20  9821  4t4e16  9825  5t4e20  9828  6t3e18  9831  6t4e24  9832  6t5e30  9833  7t3e21  9836  7t4e28  9837  7t5e35  9838  7t6e42  9839  7t7e49  9840  8t3e24  9842  8t4e32  9843  8t5e40  9844  8t7e56  9846  8t8e64  9847  9t3e27  9849  9t4e36  9850  9t5e45  9851  9t6e54  9852  9t7e63  9853  9t8e72  9854  9t9e81  9855  infrenegsupex  9944  znq  9974  ltpnf  10132  mnflt  10135  mnfltpnf  10137  xnegpnf  10180  xnegmnf  10181  xaddpnf1  10198  xaddpnf2  10199  xaddmnf1  10200  xaddmnf2  10201  pnfaddmnf  10202  mnfaddpnf  10203  lincmb01cmp  10355  iccf1o  10357  iccen  10359  elfzuz2  10383  fseq1m1p1  10451  fz0tp  10478  fz0to4untppr  10480  infssfzcldc  10618  infssfzledc  10619  nninfdcex  10621  zsupssdc  10622  flqdiv  10707  frec2uzzd  10786  frec2uzsucd  10787  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgg  10802  frecuzrdgsuctlem  10809  uzenom  10811  fzfig  10816  nnenom  10820  seqeq1  10836  seq3val  10846  seqvalcd  10847  seqf  10850  seq3p1  10851  seqovcd  10853  seqp1cd  10856  seq3feq2  10862  seq3feq  10866  monoord2  10872  ser3mono  10873  seq3split  10874  seq3caopr2  10879  iseqf1olemqk  10893  seq3f1olemqsumkj  10897  seq3f1olemstep  10900  seq3f1oleml  10902  seq3f1o  10903  seqf1og  10907  seq3homo  10913  seq3z  10914  seqfeq3  10915  seq3distr  10918  ser0f  10920  ser3ge0  10922  ser3le  10923  exp0  10929  0exp  10960  sq0  11016  sq10  11099  sq10e99m1  11100  facnn  11114  fac0  11115  bcval5  11150  hashinfom  11166  hashennn  11168  hashcl  11169  hashfz1  11171  hashen  11172  hash0  11184  fihashdom  11192  hashun  11194  hashfibclem  11231  seq3coll  11239  fundm2domnop0  11245  ccatlen  11308  ccatvalfn  11314  ccatalpha  11326  s111  11344  swrdlen  11369  swrdfv  11370  swrdwrdsymbg  11381  swrdswrd  11422  ccatlcan  11435  ccatrcan  11436  cats1un  11438  pfxccatid  11458  swrdccatin2d  11461  pfxccatin12d  11462  s2leng  11506  shftfibg  11530  shftfib  11533  shftfn  11534  2shfti  11541  seq3shft  11548  cvg1n  11696  resqrexlemsqa  11734  negfi  11938  xrmaxiflemcom  11959  xrmaxif  11961  infxrnegsupex  11973  climconst2  12001  climres  12013  climshft  12014  serclim0  12015  climle  12044  clim2ser  12047  clim2ser2  12048  climub  12054  climcvg1n  12060  climcaucn  12061  serf0  12062  sumfct  12084  fsum3cvg  12089  summodclem2  12093  zsumdc  12095  fsum3  12098  isumz  12100  fsumf1o  12101  isumss  12102  fsum3cvg2  12105  fsumsersdc  12106  fsum3ser  12108  fsumcl2lem  12109  fsumadd  12117  fsumsplitf  12119  sumsnf  12120  isummulc2  12137  isumadd  12142  fsumcnv  12148  mptfzshft  12153  fsumrev  12154  fsumshft  12155  fsummulc2  12159  iserabs  12186  isumshft  12201  isum1p  12203  isumlessdc  12207  divcnv  12208  trireciplem  12211  trirecip  12212  expcnvap0  12213  expcnvre  12214  expcnv  12215  explecnv  12216  geolim  12222  geolim2  12223  geo2lim  12227  geoisum  12228  geoisumr  12229  geoisum1  12230  geoisum1c  12231  cvgratnnlemseq  12237  cvgratz  12243  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  clim2prod  12250  clim2divap  12251  prodfap0  12256  prodfrecap  12257  prodfdivap  12258  prodeq2w  12267  fproddccvg  12283  prodmodclem2  12288  zproddc  12290  fprodseq  12294  fprodntrivap  12295  prod1dc  12297  prodfct  12298  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodmul  12302  prodsnf  12303  fprodshft  12329  fprodrev  12330  fprodcnv  12336  efcllemp  12369  efval  12372  eff  12374  efcvgfsum  12378  reefcl  12379  ege2le3  12382  ef0  12383  efcj  12384  efaddlem  12385  efadd  12386  eftlcl  12399  reeftlcl  12400  eftlub  12401  efsep  12402  effsumlt  12403  efgt1p2  12406  efgt1p  12407  eflegeo  12412  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  eirraplem  12488  eirrap  12489  egt2lt3  12491  dvdsmul2  12525  odd2np1lem  12583  bitsfzo  12666  gcd0val  12681  gcd0id  12700  bezoutlemnewy  12717  nnmindc  12755  nnminle  12756  nninfctlemfo  12761  nninfct  12762  eucalgcvga  12780  eucalg  12781  lcm0val  12787  qnumdencoprm  12915  qeqnumdivden  12916  phimul  12948  eulerthlemh  12953  eulerthlemth  12954  prmdivdiv  12959  hashgcdeq  12962  phisum  12963  odzval  12964  powm2modprm  12975  reumodprminv  12976  pythagtriplem18  13004  pcpremul  13016  pceulem  13017  pceu  13018  pczpre  13020  pczcl  13021  pcmul  13024  pcdiv  13025  pc1  13028  pczdvds  13037  pczndvds  13039  pczndvds2  13041  pcneg  13048  infpn  13084  1arithlem2  13087  1arith  13090  4sqlem3  13113  mul4sq  13117  4sqlem11  13124  4sqlem13m  13126  4sqlem17  13130  4sqlem18  13131  4sqlem19  13132  dec2dvds  13134  dec5dvds2  13136  2exp7  13157  2exp8  13158  2exp11  13159  2exp16  13160  ballotfilem2  13172  ballotfilemfrcn0  13217  ballotfilemrc  13218  ballotfilemirc  13219  ballotfi  13226  xpnnen  13229  ennnfonelemk  13235  ennnfonelemj0  13236  ennnfonelem0  13240  ennnfonelemnn0  13257  ctinfom  13263  ctiunct  13275  ssnnct  13282  nninfdclemcl  13283  nninfdclemf  13284  nninfdclemp1  13285  2strstrndx  13415  2strstr1g  13419  ressplusgd  13426  srngstrd  13443  ipsstrd  13473  elrest  13543  elrestr  13544  topnpropgd  13550  imasvalstrd  13562  prdsvalstrd  13563  imasbas  13571  imasplusg  13572  imasmulr  13573  qusin  13590  qusbas  13591  qusaddval  13599  qusaddf  13600  qusmulval  13601  qusmulf  13602  mgmsscl  13624  plusffng  13628  mgmplusf  13629  mgmb1mgm1  13631  mgm0  13632  mgm1  13633  opifismgmdc  13634  grpidpropdg  13637  0g0  13639  mgmidcl  13641  mgmlrid  13642  grpidd  13646  gsumpropd  13655  gsumpropd2  13656  gsummgmpropd  13657  gsumress  13658  gsum0g  13659  gsumval2  13660  sgrpmgm  13670  sgrp0  13673  sgrp1  13674  issgrpd  13675  sgrppropd  13676  sgrpidmndm  13681  mndsgrp  13682  mndidcl  13691  mndbn0  13692  hashfinmndnn  13693  ismndd  13698  mndpfo  13699  mndfo  13700  mndpropd  13701  issubmnd  13703  ress0g  13704  imasmnd2  13707  imasmnd  13708  imasmndf1  13709  mnd1  13710  mhmf  13720  mhmpropd  13721  mhmlin  13722  mhm0  13723  idmhm  13724  mhmf1o  13725  issubm2  13728  mndissubm  13730  submss  13731  submid  13732  subm0cl  13733  submcl  13734  submmnd  13735  submbas  13736  subm0  13737  subsubm  13738  0subm  13739  insubm  13740  0mhm  13741  resmhm  13742  resmhm2  13743  resmhm2b  13744  mhmco  13745  mhmima  13746  mhmeql  13747  gsumsubm  13749  gsumfzz  13750  gsumwsubmcl  13751  gsumwmhm  13753  gsumfzcl  13754  grpmnd  13762  grppropd  13772  isgrpd2e  13775  dfgrp2  13782  grpbn0  13785  grpn0  13790  grprcan  13792  grpidd2  13796  grpinvval  13798  grpinvfng  13799  grpsubval  13801  grpinvf  13802  grplrinv  13812  grpidinv  13814  grpinvid  13815  grpressid  13816  grplcan  13817  grpasscan1  13818  grpasscan2  13819  grpinvinv  13822  grpinvcnv  13823  grplmulf1o  13829  grpinvpropdg  13830  grpidssd  13831  grpinvssd  13832  grpinvadd  13833  grpsubf  13834  grpsubrcan  13836  grpinvsub  13837  grpinvval2  13838  grpsubid  13839  grpsubid1  13840  grpsubeq0  13841  grpsubadd0sub  13842  grpsubadd  13843  grpsubsub  13844  grpaddsubass  13845  grppncan  13846  grpnpcan  13847  grpnnncan2  13852  dfgrp3m  13854  grplactcnv  13857  grplactf1o  13858  grpsubpropdg  13859  grpsubpropd2  13860  grp1  13861  grp1inv  13862  imasgrp2  13863  imasgrp  13864  imasgrpf1  13865  qusgrp2  13866  mhmid  13868  mhmmnd  13869  mhmfmhm  13870  ghmgrp  13871  mulgex  13876  mulgfng  13877  mulg0  13878  mulgnn  13879  mulgnngsum  13880  mulgnn0gsum  13881  mulg1  13882  mulgnnp1  13883  mulgnegnn  13885  mulgnn0p1  13886  mulgnnsubcl  13887  mulgnncl  13890  mulgnn0cl  13891  mulgcl  13892  mulgneg  13893  mulgaddcomlem  13898  mulgaddcom  13899  mulginvcom  13900  mulgnn0z  13902  mulgz  13903  mulgnndir  13904  mulgnn0dir  13905  mulgdirlem  13906  mulgdir  13907  mulgneg2  13909  mulgnnass  13910  mulgnn0ass  13911  mulgass  13912  mulgmodid  13914  mulgsubdir  13915  mhmmulg  13916  mulgpropdg  13917  submmulgcl  13918  submmulg  13919  subggrp  13930  subgbas  13931  subgrcl  13932  subg0  13933  subginv  13934  subg0cl  13935  subginvcl  13936  subgcl  13937  subgsubcl  13938  subgsub  13939  subgmulgcl  13940  subgmulg  13941  issubg2m  13942  issubgrpd2  13943  issubgrpd  13944  issubg3  13945  issubg4m  13946  grpissubg  13947  subgsubm  13949  subsubg  13950  subgintm  13951  0subg  13952  nsgsubg  13958  isnsg3  13960  nmzsubg  13963  ssnmz  13964  nmznsg  13966  0nsg  13967  nsgid  13968  eqgval  13976  eqger  13977  eqglact  13978  eqgid  13979  eqgen  13980  eqgcpbl  13981  eqg0el  13982  qusgrp  13985  quseccl  13986  qusadd  13987  qus0  13988  qusinv  13989  qussub  13990  ecqusaddd  13991  ecqusaddcl  13992  ghmgrp1  13998  ghmgrp2  13999  ghmf  14000  ghmlin  14001  ghmid  14002  ghminv  14003  ghmsub  14004  ghmmhm  14006  ghmmhmb  14007  ghmmulg  14009  ghmrn  14010  idghm  14012  resghm  14013  ghmima  14018  ghmpreima  14019  ghmeql  14020  ghmnsgima  14021  ghmnsgpreima  14022  ghmeqker  14024  ghmf1  14026  kerf1ghm  14027  ghmf1o  14028  conjghm  14029  conjsubg  14030  conjsubgen  14031  conjnmz  14032  conjnsg  14034  qusghm  14035  cmnpropd  14048  iscmnd  14051  cmnmnd  14054  ablsub2inv  14064  ablsub4  14066  abladdsub4  14067  ablpncan2  14069  ablsubsub4  14072  ablpnpcan  14073  ablnncan  14074  ablsub32  14075  ablnnncan  14076  ablsubsub23  14078  invghm  14082  eqgabl  14083  subgabl  14085  subcmnd  14086  ablnsg  14087  ablressid  14088  imasabl  14089  gsumfzreidx  14090  gsumfzsubmcl  14091  gsumfzmptfidmadd  14092  gsumfzconst  14094  gsumfzmhm  14096  gsumfzmhm2  14097  gsumfzsnfd  14098  gsumsplit0  14099  gfsumval  14102  gfsum0  14104  gsumshift  14105  gsumgfsum  14106  gfsumsn  14107  gfsumz  14109  gfsumcl  14110  prdsbaslemss  14116  prdssca  14117  prdsbas  14118  prdsplusg  14119  prdsmulr  14120  prdsplusgfval  14126  prdsmulrfval  14128  prdsbas3  14129  prdsbascl  14131  prdsplusgsgrpcl  14132  prdssgrpd  14133  prdsplusgcl  14134  prdsidlem  14135  prdsmndd  14136  prds0g  14137  prdsinvlem  14138  prdsgrpd  14139  prdsinvgd  14140  pwsbas  14147  pwsplusgval  14150  pwsmulrval  14151  pwsmnd  14154  pws0g  14155  pwsgrp  14156  pwsinvg  14157  pwssub  14158  mgpex  14164  mgpbasg  14165  mgpscag  14166  mgptsetg  14167  mgptopng  14168  mgpdsg  14169  mgpress  14170  rngabl  14174  rngmgp  14175  rngmgpf  14176  rngass  14178  rngdi  14179  rngdir  14180  rngcl  14183  rnglz  14184  rngrz  14185  rngmneg1  14186  rngmneg2  14187  rngsubdi  14190  rngsubdir  14191  isrngd  14192  rngressid  14193  rngpropd  14194  imasrng  14195  imasrngf1  14196  qusrng  14197  rng1zrlem  14198  rng1zr  14199  dfur2g  14205  srgcmn  14209  srgmgp  14211  srgdilem  14212  srgcl  14213  srgass  14214  srgideu  14215  srgidcl  14219  srgidmlem  14221  issrgid  14224  srgrz  14227  srglz  14228  srg1zr  14230  srgmulgass  14232  srgpcomp  14233  srgpcompp  14234  srgpcomppsc  14235  srglmhm  14236  srgrmhm  14237  srg1expzeq1  14238  ringgrp  14244  ringmgp  14245  crngring  14251  mgpf  14254  ringdilem  14255  ringcl  14256  crngcom  14257  iscrng2  14258  ringass  14259  ringideu  14260  ringidcl  14263  ringidmlem  14265  isringid  14268  ringid  14269  ringidss  14272  ringcom  14274  ringabl  14275  ringrng  14279  ringpropd  14281  crngpropd  14282  isringd  14284  iscrngd  14285  ringlz  14286  ringrz  14287  ringsrg  14290  ring1eq0  14291  ringnegl  14294  ringnegr  14295  ringmneg1  14296  ringmneg2  14297  ringsubdi  14299  ringsubdir  14300  mulgass2  14301  ring1  14302  ringn0  14303  ringlghm  14304  ringrghm  14305  ringressid  14306  imasring  14307  imasringf1  14308  qusring2  14309  opprex  14316  opprsllem  14317  opprrng  14320  opprrngbg  14321  opprring  14322  opprringbg  14323  opprringb  14324  oppr0g  14325  oppr1g  14326  opprnegg  14327  opprsubgg  14328  mulgass3  14329  reldvdsrsrg  14337  dvdsrvald  14338  dvdsrd  14339  dvdsrmuld  14341  dvdsrex  14343  dvdsrcl2  14344  dvdsrid  14345  dvdsrtr  14346  dvdsrneg  14348  dvdsr01  14349  dvdsr02  14350  1unit  14352  opprunitd  14355  crngunit  14356  dvdsunit  14357  unitmulcl  14358  unitmulclb  14359  unitgrpbasd  14360  unitgrp  14361  unitabl  14362  unitgrpid  14363  unitsubm  14364  invrfvald  14367  unitinvcl  14368  unitinvinv  14369  unitlinv  14371  unitrinv  14372  1rinv  14373  0unit  14374  unitnegcl  14375  dvrvald  14379  dvrcl  14380  unitdvcl  14381  dvrid  14382  dvr1  14383  dvrass  14384  dvrcan1  14385  dvrcan3  14386  dvreq1  14387  dvrdir  14388  rdivmuldivd  14389  ringinvdv  14390  rngidpropdg  14391  unitpropdg  14393  invrpropdg  14394  dfrhm2  14399  rhmghm  14407  rhmmul  14409  isrhm2d  14410  rhm1  14412  rhmf1o  14413  rhmco  14419  rhmdvdsr  14420  rhmopp  14421  elrhmunit  14422  rhmunitinv  14423  isnzr2  14429  opprnzrbg  14430  ringelnzr  14432  nzrunit  14433  lringuplu  14441  opprlring  14442  subrngrng  14448  subrngrcl  14449  subrngsubg  14450  subrngringnsg  14451  subrngmcl  14455  issubrng2  14456  opprsubrngg  14457  subrngintm  14458  subsubrng  14460  subrngpropd  14462  subrgss  14468  subrgid  14469  subrgring  14470  subrgcrng  14471  subrgrcl  14472  subrgsubg  14473  subrg1cl  14475  subrg1  14477  subrgmcl  14479  subrgsubm  14480  subrgdvds  14481  subrguss  14482  subrginv  14483  subrgdv  14484  subrgunit  14485  subrgugrp  14486  issubrg2  14487  subrgnzr  14488  subrgintm  14489  subsubrg  14491  issubrg3  14493  resrhm  14494  resrhm2b  14495  rhmeql  14496  rhmima  14497  rnrhmsubrg  14498  subrgpropd  14499  rhmpropd  14500  rrgsupp  14512  rrgss  14513  unitrrg  14514  rrgnz  14515  domnnzr  14517  opprdomnbg  14521  aprunit  14530  ringunitsap0  14532  aprirr  14533  aprsym  14534  aprcotr  14535  aprap  14536  aprnzr  14537  aprlring  14538  drnglring  14545  drnguiap  14547  drngprop  14555  drngnzr  14557  opprdrng  14558  islmodd  14567  lmodgrp  14568  lmodring  14569  lmodvscl  14579  scaffng  14583  lmodscaf  14584  lmodvsdi  14585  lmodvsdir  14586  lmodvsass  14587  lmodvs1  14590  lmod0vs  14595  lmodvs0  14596  lmodvsmmulgdi  14597  lmodfopnelem1  14598  lmodfopne  14600  lmodvneg1  14604  lmodvsneg  14605  lmodcom  14607  lmodabl  14608  lmodvsubval2  14616  lmodsubvs  14617  lmodsubdi  14618  lmodsubdir  14619  lmodprop2d  14622  lmodpropd  14623  rmodislmodlem  14624  rmodislmod  14625  islssmd  14633  lssssg  14634  lss1  14636  lssclg  14638  lssvacl  14639  lssvsubcl  14640  lssvancl1  14641  lss0cl  14643  lsssn0  14644  lssvscl  14649  lssvnegcl  14650  lsssubg  14651  islss3  14653  lsslmod  14654  lsslss  14655  islss4  14656  lss1d  14657  lssintclm  14658  lspval  14664  lspex  14669  lspsnsubg  14670  lspid  14671  lspssv  14672  lspss  14673  lspssid  14674  lspidm  14675  lspssp  14677  lspsnel5a  14684  lspprid1  14685  lspprvacl  14687  lssats2  14688  lspsneli  14689  lspsn  14690  lspsnvsi  14692  lspsnss2  14693  lspsnneg  14694  lspsnsub  14695  lspsn0  14696  lsp0  14697  lspuni0  14698  lspun0  14699  lmodindp1  14702  lsslsp  14703  lss0v  14704  lsspropdg  14705  lsppropd  14706  sralmod  14724  issubrgd  14726  rlmscabas  14734  rlmlmod  14738  lidlss  14750  lidlbas  14752  islidlm  14753  rnglidlmcl  14754  dflidl2rng  14755  isridlrng  14756  lidl0cl  14757  lidlacl  14758  lidlnegcl  14759  lidlsubg  14760  lidl0  14763  lidl1  14764  rspcl  14765  rspssid  14766  rsp0  14767  rspssp  14768  rnglidlmmgm  14770  rnglidlmsgrp  14771  rnglidlrng  14772  isridl  14778  2idllidld  14780  2idlridld  14781  df2idl2rng  14782  df2idl2  14783  ridl0  14784  ridl1  14785  2idl0  14786  2idl1  14787  2idlss  14788  2idlbas  14789  2idlelbas  14790  rng2idlsubrng  14791  rng2idl0  14793  rng2idlsubgsubrng  14794  rng2idlsubg0  14796  2idlcpblrng  14797  2idlcpbl  14798  qus2idrng  14799  qus1  14800  qusring  14801  qusrhm  14802  qusmul2  14803  crngridl  14804  crng2idl  14805  qusmulrng  14806  quscrng  14807  rspsn  14808  cnfldstr  14832  cnfld0  14845  cnfld1  14846  cnfldneg  14847  cnfldplusf  14848  cnfldsub  14849  cnfldmulg  14850  cnfldexp  14851  cnsubglem  14853  zsssubrg  14859  gsumfzfsumlemm  14861  cnfldui  14863  zringmulg  14872  zringinvg  14878  zringmpg  14880  expghmap  14881  mulgghm2  14882  mulgrhm  14883  mulgrhm2  14884  zrhval2  14893  zrhmulg  14894  zrhrhmb  14896  zrhrhm  14897  zrhpropd  14900  zlmlemg  14902  zlmsca  14906  znlidl  14908  zncrng2  14909  znval  14910  znle  14911  znval2  14912  znbaslemnn  14913  zncrng  14919  znzrh2  14920  znzrhval  14921  znzrhfo  14922  zndvds  14923  znf1o  14925  znle2  14926  znleval  14927  znfi  14929  znhash  14930  znidom  14931  znidomb  14932  znunit  14933  znrrg  14934  psrvalstrd  14942  fczpsrbag  14946  psrbagconf1o  14954  psrbasg  14955  psrelbasfi  14957  psrelbasfun  14958  psrplusgg  14959  psraddcl  14961  psr0cl  14962  psr0lid  14963  psrnegcl  14964  psrlinv  14965  psrgrp  14966  psr0  14967  psrneg  14968  psr1clfi  14969  mplbascoe  14972  mplval2g  14976  mplbasss  14977  mplelf  14978  mplsubgfilemm  14979  mplsubgfilemcl  14980  mplsubgfileminv  14981  mplsubgfi  14982  mpl0fi  14983  mplplusgg  14984  mpladd  14985  mplnegfi  14986  mplgrpfi  14987  toptopon2  15010  toponmax  15016  tpstop  15026  tpspropd  15027  tsettps  15029  eltpsg  15031  tgiun  15064  ntrval  15101  clsval  15102  0cld  15103  uncld  15104  cldcls  15105  ntr0  15125  isopn3i  15126  neif  15132  neival  15134  neii2  15140  neiss  15141  opnneiss  15149  innei  15154  neissex  15156  tgrest  15160  stoig  15164  restco  15165  resttopon2  15169  restopn2  15174  cnpval  15189  cntop1  15192  cntop2  15193  cnprcl2k  15197  lmcvg  15208  iscnp4  15209  cnima  15211  cnco  15212  cnclima  15214  cnntri  15215  cnntr  15216  cnss1  15217  cnss2  15218  cncnpi  15219  cncnp  15221  cnrest  15226  cnrest2  15227  cnrest2r  15228  lmss  15237  lmres  15239  lmcn  15242  txuni2  15247  txbasex  15248  eltx  15250  txtop  15251  txtopon  15253  txopn  15256  txss12  15257  txbasval  15258  neitx  15259  txcnp  15262  upxp  15263  txcnmpt  15264  uptx  15265  txcn  15266  txrest  15267  txdis1cn  15269  txlm  15270  lmcn2  15271  cnmpt11  15274  cnmpt11f  15275  cnmpt1t  15276  cnmpt12  15278  cnmpt21  15282  cnmpt21f  15283  cnmpt2t  15284  cnmpt22  15285  cnmpt1res  15287  cnmpt2res  15288  cnmptcom  15289  imasnopn  15290  hmeocnv  15298  hmeoopn  15302  hmeocld  15303  hmeontr  15304  hmeoimaf1o  15305  hmeores  15306  txhmeo  15310  txswaphmeo  15312  xmet0  15354  blfvalps  15376  blfps  15400  blf  15401  blpnfctr  15430  xmetresbl  15431  isxms2  15443  xmstps  15448  msxms  15449  xmsxmet  15451  msmet  15452  xmspropd  15468  mspropd  15469  neibl  15482  bdxmet  15492  bdmopn  15495  mopnex  15496  xmetxp  15498  xmettxlem  15500  xmettx  15501  txmetcnp  15509  metcnpd  15511  cnmet  15521  cnfldms  15527  cnfldtopn  15530  unicntopcntop  15533  unicntop  15534  cnopncntop  15535  cnopn  15536  remetdval  15538  resubmet  15547  tgioo2cntop  15548  tgioo2  15550  addcncntoplem  15552  divcnap  15556  fsumcncntop  15558  expcn  15560  divccncfap  15581  cncfmet  15583  cncfcncntop  15584  cncfmptc  15587  cncfmptid  15588  cncfmpt1f  15589  cncfmpt2fcntop  15590  sub1cncf  15593  sub2cncf  15594  cdivcncfap  15595  negfcncf  15597  mulcncflem  15598  mulcncf  15599  cnopnap  15602  addcncf  15603  subcncf  15604  divcncfap  15605  ivthinc  15634  ivthdec  15635  ivthreinc  15636  hovercncf  15637  limcmpted  15654  limcimolemlt  15655  cnplimcim  15658  cnplimclemr  15660  cnlimcim  15662  cnlimc  15663  cnmptlimc  15665  limccnpcntop  15666  limccnp2lem  15667  limccnp2cntop  15668  reldvg  15670  dvfvalap  15672  dvcl  15674  dvbss  15676  dvfgg  15679  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvcn  15691  dvaddxxbr  15692  dvmulxxbr  15693  dvaddxx  15694  dvmulxx  15695  dviaddf  15696  dvimulf  15697  dvcoapbr  15698  dvcjbr  15699  dvrecap  15704  dveflem  15717  dvef  15718  elply2  15726  elplyd  15732  plypow  15735  plyconst  15736  plyaddlem  15740  plymullem  15741  plycoeid3  15748  plycn  15753  plyrecj  15754  dvply1  15756  dvply2g  15757  sincn  15760  coscn  15761  wilthlem1  15974  mpodvdsmulf1o  15984  fsumdvdsmul  15985  sgmppw  15986  0sgmppw  15987  sgmmul  15990  lgsfcl  16007  lgsfle1  16008  lgsval4lem  16010  lgscl2  16011  lgs0  16012  lgscl  16013  lgsle1  16014  lgsval2  16015  lgs2  16016  lgsval4  16019  lgsfcl3  16020  lgsneg  16023  lgsmod  16025  lgsdirprm  16033  lgsdir  16034  lgsdi  16036  lgsne0  16037  lgseisenlem3  16071  lgseisenlem4  16072  lgseisen  16073  lgsquadlem3  16078  lgsquad  16079  2lgslem1  16090  2lgs  16103  2sqlem9  16123  uhgrfun  16198  uhgrm  16199  lpvtx  16200  ushgruhgr  16201  isuhgropm  16202  uhgr0e  16203  uhgr0vb  16205  uhgrun  16207  incistruhgr  16211  upgrop  16225  upgruhgr  16232  umgrupgr  16233  umgrnloopv  16235  umgrnloop  16237  umgr0e  16239  upgr1edc  16242  upgr1eopdc  16244  upgr1een  16245  umgr1een  16246  upgrun  16247  umgrun  16249  lfgredg2dom  16253  uhgriedg0edg0  16256  uhgredgm  16257  upgredgssen  16260  umgredgssen  16261  edgupgren  16262  edgumgren  16263  upgredg  16265  umgrnloop2  16272  usgrfun  16282  usgredgssen  16283  isuspgropen  16285  isusgropen  16286  usgrop  16287  ausgrusgrben  16289  ausgrumgrien  16291  ausgrusgrien  16292  usgrf1o  16295  uspgrf1oedg  16297  uspgrushgr  16301  uspgrupgr  16302  uspgrupgrushgr  16303  usgruspgr  16304  usgrumgr  16305  usgrumgruspgr  16306  usgruspgrben  16307  usgredg2en  16316  umgr2edg  16328  umgrvad2edg  16332  usgrsizedgen  16334  usgredg3  16335  usgredg2vtx  16338  uspgredg2vtxeu  16339  usgredg2v  16345  usgriedgdomord  16346  ushgredgedg  16347  ushgredgedgloop  16349  uspgredgdomord  16350  usgrstrrepeen  16352  usgr0e  16353  uhgr0enedgfi  16357  uhgr0vusgr  16359  uspgr1edc  16361  uspgr1eopdc  16364  usgr1eop  16366  usgr1vr  16369  usgrprc  16373  uhgrissubgr  16382  subgrprop3  16383  egrsubgr  16384  0grsubgr  16385  0uhgrsubgr  16386  uhgrsubgrself  16387  subgrfun  16388  subgruhgrfun  16389  subgreldmiedg  16390  subgruhgredgdm  16391  subumgredg2en  16392  subuhgr  16393  subupgr  16394  subumgr  16395  subusgr  16396  uhgrspansubgr  16398  vtxdgfifival  16412  vtxdgop  16413  vtxdgfi0e  16416  vtxdeqd  16417  vtxdfifiun  16418  vtxdumgrfival  16419  vtxd0nedgbfi  16420  vtxduspgrfvedgfilem  16421  vtxduspgrfvedgfi  16422  vtxdusgrfvedgfi  16423  1loopgruspgr  16424  1loopgrvd2fi  16426  1loopgrvd0fi  16427  1hevtxdg0fi  16428  1hevtxdg1en  16429  1hegrvtxdg1fi  16430  p1evtxdeqfilem  16432  p1evtxdeqfi  16433  wlkex  16446  wlkv  16447  wlkvg  16449  wlkf  16451  wlkfg  16452  wlkcl  16453  wlkclg  16454  wlkp  16455  wlkpg  16456  wlklenvp1  16458  wlklenvp1g  16459  wlkm  16460  wlkvtxm  16461  wlkvtxeledgg  16465  wlkvtxiedg  16466  wlkvtxiedgg  16467  wlkeq  16475  wlkl1loop  16479  wlk1walkdom  16480  upgriswlkdc  16481  upgrwlkedg  16482  wlkvtxedg  16484  upgrwlkvtxedg  16485  uspgr2wlkeq  16486  umgrwlknloop  16489  wlkv0  16490  wlkres  16500  clwwlkbp  16516  clwwlkgt0  16517  clwwlksswrd  16518  clwwlk1loop  16520  clwwlkccat  16522  umgrclwwlkge2  16523  clwwlkng  16526  isclwwlkng  16527  isclwwlkn  16534  clwwlkn1  16539  clwwlkn2  16542  clwwlknccat  16544  umgr2cwwk2dif  16545  clwwlknonmpo  16549  clwwlknon  16550  clwwlknonccat  16554  clwwlknonex2lem2  16559  clwwlknun  16562  eupthv  16567  eupthcl  16574  eupthistrl  16575  eupthpf  16577  eupthres  16578  trlsegvdegfi  16588  eupth2lem3lem1fi  16589  eupth2lem3lem2fi  16590  eupth2lembfi  16598  eupth2lemsfi  16599  eupth2fi  16600  eulerpathprum  16601  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  ex-or  16616  ex-an  16617  1kp2ke3k  16618  ex-exp  16621  ex-fac  16622  depindlem1  16627  depind  16630  fnmptd  16702  bj-2inf  16834  bj-inf2vnlem1  16866  pw1map  16895  pw1mapen  16896  subctctexmid  16900  exmidcon  16906  nnsf  16909  peano3nninf  16911  nninfself  16917  nninfsellemeqinf  16920  nninffeq  16924  nnnninfex  16926  nninfnfiinf  16927  iooreen  16945  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  iswomni0  16962  dceqnconst  16972  dcapnconst  16973  nconstwlpolemgt0  16976