Theorem eqid 2177

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 2174	1 ⊢ 𝐴 = 𝐴

Syntax hints:   = wceq 1353   ∈ wcel 2148

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 1449  ax-ext 2159

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

This theorem is referenced by:  eqidd  2178  neirr  2356  sbsbc  2967  sbceqal  3019  dfnul2  3425  snidg  3622  prid1g  3697  tpid1  3704  tpid1g  3705  tpid2  3706  tpid2g  3707  tpid3  3709  dfiin2g  3920  eqbrtrid  4039  eqbrtrrid  4040  breqtrdi  4045  opabbii  4071  mpteq2ia  4090  mpteq2da  4093  sucidg  4417  onsucelsucexmidlem1  4528  regexmidlemm  4532  regexmidlem1  4533  reg2exmidlema  4534  regexmid  4535  reg2exmid  4536  reg3exmid  4580  tfisi  4587  finds1  4602  nn0suc  4604  nndceq0  4618  0elnn  4619  nnregexmid  4621  opelxp  4657  relopab  4754  relop  4778  ididg  4781  elrnmpt1s  4878  dfiun3g  4885  dfiin3g  4886  dmmptg  5127  funfn  5247  mpt0  5344  f0  5407  dffn4  5445  f1orn  5472  f1oabexg  5474  f1o00  5497  f1o0  5499  fnbrfvb  5557  fnrnfv  5563  funfvdm  5580  fvmptg  5593  fvmptd  5598  fvmpt2d  5603  fvmptdf  5604  mpteqb  5607  fvmptt  5608  fnmptfvd  5621  funfvop  5629  eldmrexrn  5658  fvmptelcdm  5670  fmpttd  5672  fmpt2d  5679  fmptco  5683  fmptcof  5684  fnasrn  5695  fnasrng  5697  mptexg  5742  eufnfv  5748  idref  5758  f1elima  5774  fliftrel  5793  fliftel  5794  fliftel1  5795  fliftcnv  5796  fliftf  5800  riotabiia  5848  acexmidlem2  5872  acexmidlemv  5873  oprabbii  5930  mpoeq12  5935  ovmpodxf  6000  ovmpodf  6006  ov6g  6012  f1ocnvd  6073  f1opw2  6077  suppssfv  6079  suppssov1  6080  ofvalg  6092  off  6095  offval2  6098  ofrfval2  6099  caofinvl  6105  mptexw  6114  abrexex  6118  abrexexg  6119  offres  6136  ofmres  6137  op1steq  6180  reldm  6187  mpoexga  6213  mpoexw  6214  mpoex  6215  fnmpoovd  6216  fmpoco  6217  cnvf1o  6226  f1od2  6236  tposssxp  6250  brtpos2  6252  tpos0  6275  iunon  6285  tfrfun  6321  tfr2a  6322  tfrlemisucfn  6325  tfri1d  6336  tfr1onlemsucfn  6341  tfr1onlemubacc  6347  tfr1on  6351  tfri1dALT  6352  tfrcllemubacc  6360  tfrex  6369  rdgfun  6374  rdgon  6387  rdg0  6388  frec0g  6398  frecfnom  6402  freccllem  6403  freccl  6404  frecfcllem  6405  frecfcl  6406  frecsuclem  6407  0lt1o  6441  oafnex  6445  omfnex  6450  fnoei  6453  oeiexg  6454  oeiv  6457  oacl  6461  omcl  6462  oeicl  6463  oav2  6464  omv2  6466  eqer  6567  ecelqsg  6588  elqsn0m  6603  qsel  6612  qliftf  6620  ecoptocl  6622  eroprf  6628  ecopovsym  6631  ecopovtrn  6632  ecopovsymg  6634  ecopovtrng  6635  th3qlem2  6638  th3q  6640  mapsncnv  6695  mapsnf1o3  6697  mptelixpg  6734  ixpsnf1o  6736  en2d  6768  en3d  6769  dom2lem  6772  dom2  6775  1domsn  6819  xpcomen  6827  xpf1o  6844  mapxpen  6848  fidifsnen  6870  isbth  6966  elfir  6972  supsnti  7004  djueq1  7039  djueq2  7040  djuf1olem  7052  inl11  7064  updjud  7081  omp1eom  7094  difinfsn  7099  ctmlemr  7107  ctssdclemn0  7109  ctssdclemr  7111  ctssdc  7112  enumct  7114  infnninf  7122  nnnninf  7124  nnnninfeq  7126  nninfisollemne  7129  nninfisol  7131  ismkvnex  7153  mkvprop  7156  nninfwlporlemd  7170  nninfwlpoimlemginf  7174  exmidonfin  7193  exmidaclem  7207  exmidac  7208  cc3  7267  0npi  7312  indpi  7341  recidnq  7392  addnnnq0  7448  mulnnnq0  7449  genpprecll  7513  genppreclu  7514  caucvgprpr  7711  addsrpr  7744  mulsrpr  7745  0nsr  7748  00sr  7768  caucvgsrlemgt1  7794  opelreal  7826  eqresr  7835  axprecex  7879  nntopi  7893  axpre-suploc  7901  ltxrlt  8023  pncan3  8165  apreim  8560  divcanap2  8637  divcanap3  8655  lble  8904  sup3exmid  8914  nn1gt1  8953  0nn0  9191  pnf0xnn0  9246  0z  9264  decaddm10  9442  decmulnc  9450  10p10e20  9478  4t4e16  9482  5t4e20  9485  6t3e18  9488  6t4e24  9489  6t5e30  9490  7t3e21  9493  7t4e28  9494  7t5e35  9495  7t6e42  9496  7t7e49  9497  8t3e24  9499  8t4e32  9500  8t5e40  9501  8t7e56  9503  8t8e64  9504  9t3e27  9506  9t4e36  9507  9t5e45  9508  9t6e54  9509  9t7e63  9510  9t8e72  9511  9t9e81  9512  infrenegsupex  9594  znq  9624  ltpnf  9780  mnflt  9783  mnfltpnf  9785  xnegpnf  9828  xnegmnf  9829  xaddpnf1  9846  xaddpnf2  9847  xaddmnf1  9848  xaddmnf2  9849  pnfaddmnf  9850  mnfaddpnf  9851  lincmb01cmp  10003  iccf1o  10004  iccen  10006  elfzuz2  10029  fseq1m1p1  10095  fz0tp  10122  fz0to4untppr  10124  flqdiv  10321  frec2uzzd  10400  frec2uzsucd  10401  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgg  10416  frecuzrdgsuctlem  10423  uzenom  10425  fzfig  10430  nnenom  10434  seqeq1  10448  seq3val  10458  seqvalcd  10459  seqf  10461  seq3p1  10462  seqovcd  10463  seqp1cd  10466  seq3feq2  10470  seq3feq  10472  monoord2  10477  ser3mono  10478  seq3split  10479  seq3caopr2  10482  iseqf1olemqk  10494  seq3f1olemqsumkj  10498  seq3f1olemstep  10501  seq3f1oleml  10503  seq3f1o  10504  seq3homo  10510  seq3z  10511  seqfeq3  10512  seq3distr  10513  ser0f  10515  ser3ge0  10517  ser3le  10518  exp0  10524  0exp  10555  sq0  10611  sq10  10692  sq10e99m1  10693  facnn  10707  fac0  10708  bcval5  10743  hashinfom  10758  hashennn  10760  hashcl  10761  hashfz1  10763  hashen  10764  hash0  10776  fihashdom  10783  hashun  10785  seq3coll  10822  shftfibg  10829  shftfib  10832  shftfn  10833  2shfti  10840  seq3shft  10847  cvg1n  10995  resqrexlemsqa  11033  negfi  11236  xrmaxiflemcom  11257  xrmaxif  11259  infxrnegsupex  11271  climconst2  11299  climres  11311  climshft  11312  serclim0  11313  climle  11342  clim2ser  11345  clim2ser2  11346  climub  11352  climcvg1n  11358  climcaucn  11359  serf0  11360  sumfct  11382  fsum3cvg  11386  summodclem2  11390  zsumdc  11392  fsum3  11395  isumz  11397  fsumf1o  11398  isumss  11399  fsum3cvg2  11402  fsumsersdc  11403  fsum3ser  11405  fsumcl2lem  11406  fsumadd  11414  fsumsplitf  11416  sumsnf  11417  isummulc2  11434  isumadd  11439  fsumcnv  11445  mptfzshft  11450  fsumrev  11451  fsumshft  11452  fsummulc2  11456  iserabs  11483  isumshft  11498  isum1p  11500  isumlessdc  11504  divcnv  11505  trireciplem  11508  trirecip  11509  expcnvap0  11510  expcnvre  11511  expcnv  11512  explecnv  11513  geolim  11519  geolim2  11520  geo2lim  11524  geoisum  11525  geoisumr  11526  geoisum1  11527  geoisum1c  11528  cvgratnnlemseq  11534  cvgratz  11540  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  clim2prod  11547  clim2divap  11548  prodfap0  11553  prodfrecap  11554  prodfdivap  11555  prodeq2w  11564  fproddccvg  11580  prodmodclem2  11585  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prod1dc  11594  prodfct  11595  fprodf1o  11596  prodssdc  11597  fprodssdc  11598  fprodmul  11599  prodsnf  11600  fprodshft  11626  fprodrev  11627  fprodcnv  11633  efcllemp  11666  efval  11669  eff  11671  efcvgfsum  11675  reefcl  11676  ege2le3  11679  ef0  11680  efcj  11681  efaddlem  11682  efadd  11683  eftlcl  11696  reeftlcl  11697  eftlub  11698  efsep  11699  effsumlt  11700  efgt1p2  11703  efgt1p  11704  eflegeo  11709  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  eirraplem  11784  eirrap  11785  egt2lt3  11787  dvdsmul2  11821  odd2np1lem  11877  nninfdcex  11954  zsupssdc  11955  gcd0val  11961  gcd0id  11980  bezoutlemnewy  11997  nnmindc  12035  nnminle  12036  eucalgcvga  12058  eucalg  12059  lcm0val  12065  qnumdencoprm  12193  qeqnumdivden  12194  phimul  12226  eulerthlemh  12231  eulerthlemth  12232  prmdivdiv  12237  hashgcdeq  12239  phisum  12240  odzval  12241  powm2modprm  12252  reumodprminv  12253  pythagtriplem18  12281  pcpremul  12293  pceulem  12294  pceu  12295  pczpre  12297  pczcl  12298  pcmul  12301  pcdiv  12302  pc1  12305  pczdvds  12313  pczndvds  12315  pczndvds2  12317  pcneg  12324  infpn  12359  1arithlem2  12362  1arith  12365  4sqlem3  12388  mul4sq  12392  xpnnen  12395  ennnfonelemk  12401  ennnfonelemj0  12402  ennnfonelem0  12406  ennnfonelemnn0  12423  ctinfom  12429  ctiunct  12441  ssnnct  12448  nninfdclemcl  12449  nninfdclemf  12450  nninfdclemp1  12451  2strstr1g  12580  ressplusgd  12587  srngstrd  12604  ipsstrd  12634  elrest  12695  elrestr  12696  topnpropgd  12702  imasbas  12728  imasplusg  12729  imasmulr  12730  qusin  12746  qusbas  12747  qusaddval  12754  qusaddf  12755  qusmulval  12756  qusmulf  12757  mgmsscl  12780  plusffng  12784  mgmplusf  12785  mgmb1mgm1  12787  mgm0  12788  mgm1  12789  opifismgmdc  12790  grpidpropdg  12793  0g0  12795  mgmidcl  12797  mgmlrid  12798  grpidd  12802  sgrpmgm  12813  sgrp0  12815  sgrp1  12816  sgrpidmndm  12821  mndsgrp  12822  mndidcl  12831  mndbn0  12832  hashfinmndnn  12833  ismndd  12838  mndpfo  12839  mndfo  12840  mndpropd  12841  issubmnd  12843  ress0g  12844  mnd1  12847  mhmf  12856  mhmpropd  12857  mhmlin  12858  mhm0  12859  idmhm  12860  mhmf1o  12861  issubm2  12864  mndissubm  12866  submss  12867  submid  12868  subm0cl  12869  submcl  12870  0subm  12871  insubm  12872  0mhm  12873  mhmco  12874  mhmima  12875  mhmeql  12876  grpmnd  12884  grppropd  12893  isgrpd2e  12896  dfgrp2  12902  grpbn0  12905  grpn0  12908  grprcan  12910  grpidd2  12914  grpinvval  12916  grpinvfng  12917  grpsubval  12919  grpinvf  12920  grplrinv  12927  grpidinv  12929  grpinvid  12930  grpressid  12931  grplcan  12932  grpasscan1  12933  grpasscan2  12934  grpinvinv  12937  grpinvcnv  12938  grplmulf1o  12944  grpinvpropdg  12945  grpidssd  12946  grpinvssd  12947  grpinvadd  12948  grpsubf  12949  grpsubrcan  12951  grpinvsub  12952  grpinvval2  12953  grpsubid  12954  grpsubid1  12955  grpsubeq0  12956  grpsubadd0sub  12957  grpsubadd  12958  grpsubsub  12959  grpaddsubass  12960  grppncan  12961  grpnpcan  12962  grpnnncan2  12967  dfgrp3m  12969  grplactcnv  12972  grplactf1o  12973  grpsubpropdg  12974  grpsubpropd2  12975  grp1  12976  grp1inv  12977  mhmid  12979  mhmmnd  12980  mhmfmhm  12981  ghmgrp  12982  mulgfng  12987  mulg0  12988  mulgnn  12989  mulg1  12990  mulgnnp1  12991  mulgnegnn  12993  mulgnn0p1  12994  mulgnnsubcl  12995  mulgnncl  12998  mulgnn0cl  12999  mulgcl  13000  mulgneg  13001  mulgaddcomlem  13006  mulgaddcom  13007  mulginvcom  13008  mulgnn0z  13010  mulgz  13011  mulgnndir  13012  mulgnn0dir  13013  mulgdirlem  13014  mulgdir  13015  mulgneg2  13017  mulgnnass  13018  mulgnn0ass  13019  mulgass  13020  mulgmodid  13022  mulgsubdir  13023  mhmmulg  13024  mulgpropdg  13025  submmulgcl  13026  subggrp  13037  subgbas  13038  subgrcl  13039  subg0  13040  subginv  13041  subg0cl  13042  subginvcl  13043  subgcl  13044  subgsubcl  13045  subgsub  13046  subgmulgcl  13047  subgmulg  13048  issubg2m  13049  issubgrpd2  13050  issubgrpd  13051  issubg3  13052  issubg4m  13053  grpissubg  13054  subgsubm  13056  subsubg  13057  subgintm  13058  0subg  13059  nsgsubg  13065  isnsg3  13067  nmzsubg  13070  ssnmz  13071  nmznsg  13073  0nsg  13074  nsgid  13075  eqgval  13082  eqger  13083  eqglact  13084  eqgid  13085  eqgen  13086  eqgcpbl  13087  cmnpropd  13098  iscmnd  13101  cmnmnd  13104  ablsub2inv  13114  ablsub4  13116  abladdsub4  13117  ablpncan2  13119  ablsubsub4  13122  ablpnpcan  13123  ablnncan  13124  ablsub32  13125  ablnnncan  13126  ablsubsub23  13128  subcmnd  13129  mgpex  13135  mgpbasg  13136  mgpscag  13137  mgptsetg  13138  mgptopng  13139  mgpdsg  13140  mgpress  13141  dfur2g  13145  srgcmn  13149  srgmgp  13151  srgdilem  13152  srgcl  13153  srgass  13154  srgideu  13155  srgidcl  13159  srgidmlem  13161  issrgid  13164  srgrz  13167  srglz  13168  srg1zr  13170  srgmulgass  13172  srgpcomp  13173  srgpcompp  13174  srgpcomppsc  13175  srglmhm  13176  srgrmhm  13177  srg1expzeq1  13178  ringgrp  13184  ringmgp  13185  crngring  13191  mgpf  13194  ringdilem  13195  ringcl  13196  crngcom  13197  iscrng2  13198  ringass  13199  ringideu  13200  ringidcl  13203  ringidmlem  13205  isringid  13208  ringid  13209  ringidss  13212  ringcom  13214  ringabl  13215  ringpropd  13217  crngpropd  13218  isringd  13220  iscrngd  13221  ringlz  13222  ringrz  13223  ringsrg  13224  ring1eq0  13225  ringnegl  13228  ringnegr  13229  ringmneg1  13230  ringmneg2  13231  ringsubdi  13233  ringsubdir  13234  mulgass2  13235  ring1  13236  ringn0  13237  ringressid  13238  opprex  13245  opprsllem  13246  opprring  13249  opprringbg  13250  oppr0g  13251  oppr1g  13252  opprnegg  13253  mulgass3  13254  reldvdsrsrg  13261  dvdsrvald  13262  dvdsrd  13263  dvdsrmuld  13265  dvdsrex  13267  dvdsrcl2  13268  dvdsrid  13269  dvdsrtr  13270  dvdsrneg  13272  dvdsr01  13273  dvdsr02  13274  1unit  13276  opprunitd  13279  crngunit  13280  dvdsunit  13281  unitmulcl  13282  unitmulclb  13283  unitgrpbasd  13284  unitgrp  13285  unitabl  13286  unitgrpid  13287  unitsubm  13288  invrfvald  13291  unitinvcl  13292  unitinvinv  13293  unitlinv  13295  unitrinv  13296  1rinv  13297  0unit  13298  unitnegcl  13299  dvrvald  13303  dvrcl  13304  unitdvcl  13305  dvrid  13306  dvr1  13307  dvrass  13308  dvrcan1  13309  dvrcan3  13310  dvreq1  13311  dvrdir  13312  rdivmuldivd  13313  ringinvdv  13314  rngidpropdg  13315  unitpropdg  13317  invrpropdg  13318  ringelnzr  13328  nzrunit  13329  lringuplu  13337  subrgss  13343  subrgid  13344  subrgring  13345  subrgcrng  13346  subrgrcl  13347  subrgsubg  13348  subrg1cl  13350  subrg1  13352  subrgmcl  13354  subrgsubm  13355  subrgdvds  13356  subrguss  13357  subrginv  13358  subrgdv  13359  subrgunit  13360  subrgugrp  13361  issubrg2  13362  subrgnzr  13363  subrgintm  13364  subsubrg  13366  issubrg3  13368  subrgpropd  13369  aprirr  13373  aprsym  13374  aprcotr  13375  aprap  13376  islmodd  13383  lmodgrp  13384  lmodring  13385  lmodvscl  13395  scaffng  13399  lmodscaf  13400  lmodvsdi  13401  lmodvsdir  13402  lmodvsass  13403  lmodvs1  13406  lmod0vs  13411  lmodvs0  13412  lmodvsmmulgdi  13413  lmodfopnelem1  13414  lmodfopne  13416  lmodvneg1  13420  lmodvsneg  13421  lmodcom  13423  lmodabl  13424  lmodvsubval2  13432  lmodsubvs  13433  lmodsubdi  13434  lmodsubdir  13435  lmodprop2d  13438  lmodpropd  13439  rmodislmodlem  13440  rmodislmod  13441  cnfld0  13468  cnfld1  13469  cnfldneg  13470  cnfldplusf  13471  cnfldsub  13472  cnfldmulg  13473  cnfldexp  13474  cnsubglem  13476  zsssubrg  13482  zringmulg  13491  zringinvg  13497  zringmpg  13499  toptopon2  13522  toponmax  13528  tpstop  13538  tpspropd  13539  tsettps  13541  eltpsg  13543  tgiun  13576  ntrval  13613  clsval  13614  0cld  13615  uncld  13616  cldcls  13617  ntr0  13637  isopn3i  13638  neif  13644  neival  13646  neii2  13652  neiss  13653  opnneiss  13661  innei  13666  neissex  13668  tgrest  13672  stoig  13676  restco  13677  resttopon2  13681  restopn2  13686  cnpval  13701  cntop1  13704  cntop2  13705  cnprcl2k  13709  lmcvg  13720  iscnp4  13721  cnima  13723  cnco  13724  cnclima  13726  cnntri  13727  cnntr  13728  cnss1  13729  cnss2  13730  cncnpi  13731  cncnp  13733  cnrest  13738  cnrest2  13739  cnrest2r  13740  lmss  13749  lmres  13751  lmcn  13754  txuni2  13759  txbasex  13760  eltx  13762  txtop  13763  txtopon  13765  txopn  13768  txss12  13769  txbasval  13770  neitx  13771  txcnp  13774  upxp  13775  txcnmpt  13776  uptx  13777  txcn  13778  txrest  13779  txdis1cn  13781  txlm  13782  lmcn2  13783  cnmpt11  13786  cnmpt11f  13787  cnmpt1t  13788  cnmpt12  13790  cnmpt21  13794  cnmpt21f  13795  cnmpt2t  13796  cnmpt22  13797  cnmpt1res  13799  cnmpt2res  13800  cnmptcom  13801  imasnopn  13802  hmeocnv  13810  hmeoopn  13814  hmeocld  13815  hmeontr  13816  hmeoimaf1o  13817  hmeores  13818  txhmeo  13822  txswaphmeo  13824  xmet0  13866  blfvalps  13888  blfps  13912  blf  13913  blpnfctr  13942  xmetresbl  13943  isxms2  13955  xmstps  13960  msxms  13961  xmsxmet  13963  msmet  13964  xmspropd  13980  mspropd  13981  neibl  13994  bdxmet  14004  bdmopn  14007  mopnex  14008  xmetxp  14010  xmettxlem  14012  xmettx  14013  txmetcnp  14021  metcnpd  14023  cnmet  14033  unicntopcntop  14039  cnopncntop  14040  remetdval  14042  resubmet  14051  tgioo2cntop  14052  addcncntoplem  14054  divcnap  14058  fsumcncntop  14059  divccncfap  14080  cncfmet  14082  cncfcncntop  14083  cncfmptc  14085  cncfmptid  14086  cncfmpt1f  14087  cncfmpt2fcntop  14088  cdivcncfap  14090  negfcncf  14092  mulcncflem  14093  mulcncf  14094  cnopnap  14097  ivthinc  14124  ivthdec  14125  limcmpted  14135  limcimolemlt  14136  cnplimcim  14139  cnplimclemr  14141  cnlimcim  14143  cnlimc  14144  cnmptlimc  14146  limccnpcntop  14147  limccnp2lem  14148  limccnp2cntop  14149  reldvg  14151  dvfvalap  14153  dvcl  14155  dvbss  14157  dvfgg  14160  dvidlemap  14163  dvcnp2cntop  14166  dvcn  14167  dvaddxxbr  14168  dvmulxxbr  14169  dvaddxx  14170  dvmulxx  14171  dviaddf  14172  dvimulf  14173  dvcoapbr  14174  dvcjbr  14175  dvrecap  14180  dveflem  14190  dvef  14191  sincn  14193  coscn  14194  lgsfcl  14412  lgsfle1  14413  lgsval4lem  14415  lgscl2  14416  lgs0  14417  lgscl  14418  lgsle1  14419  lgsval2  14420  lgs2  14421  lgsval4  14424  lgsfcl3  14425  lgsneg  14428  lgsmod  14430  lgsdirprm  14438  lgsdir  14439  lgsdi  14441  lgsne0  14442  2sqlem9  14474  ex-or  14477  ex-an  14478  1kp2ke3k  14479  ex-exp  14482  ex-fac  14483  fnmptd  14559  bj-2inf  14693  bj-inf2vnlem1  14725  subctctexmid  14753  nnsf  14757  peano3nninf  14759  nninfself  14765  nninfsellemeqinf  14768  nninffeq  14772  iooreen  14786  trilpolemcl  14788  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  iswomni0  14802  dceqnconst  14810  dcapnconst  14811  nconstwlpolemgt0  14814