Theorem eqid 2175

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	|- A = A

Proof of Theorem eqid

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		biid 171	. 2 |- ( x e. A <-> x e. A )
2	1	eqriv 2172	1 |- A = A

Syntax hints:   = wceq 1353   e. wcel 2146

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 1447  ax-ext 2157

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

This theorem is referenced by:  eqidd  2176  neirr  2354  sbsbc  2964  sbceqal  3016  dfnul2  3422  snidg  3618  prid1g  3693  tpid1  3700  tpid1g  3701  tpid2  3702  tpid2g  3703  tpid3  3705  dfiin2g  3915  eqbrtrid  4033  eqbrtrrid  4034  breqtrdi  4039  opabbii  4065  mpteq2ia  4084  mpteq2da  4087  sucidg  4410  onsucelsucexmidlem1  4521  regexmidlemm  4525  regexmidlem1  4526  reg2exmidlema  4527  regexmid  4528  reg2exmid  4529  reg3exmid  4573  tfisi  4580  finds1  4595  nn0suc  4597  nndceq0  4611  0elnn  4612  nnregexmid  4614  opelxp  4650  relopab  4747  relop  4770  ididg  4773  elrnmpt1s  4870  dfiun3g  4877  dfiin3g  4878  dmmptg  5118  funfn  5238  mpt0  5335  f0  5398  dffn4  5436  f1orn  5463  f1oabexg  5465  f1o00  5488  f1o0  5490  fnbrfvb  5548  fnrnfv  5554  funfvdm  5571  fvmptg  5584  fvmptd  5589  fvmpt2d  5594  fvmptdf  5595  mpteqb  5598  fvmptt  5599  fnmptfvd  5612  funfvop  5620  eldmrexrn  5649  fvmptelcdm  5661  fmpttd  5663  fmpt2d  5670  fmptco  5674  fmptcof  5675  fnasrn  5686  fnasrng  5688  mptexg  5733  eufnfv  5738  idref  5748  f1elima  5764  fliftrel  5783  fliftel  5784  fliftel1  5785  fliftcnv  5786  fliftf  5790  riotabiia  5838  acexmidlem2  5862  acexmidlemv  5863  oprabbii  5920  mpoeq12  5925  ovmpodxf  5990  ovmpodf  5996  ov6g  6002  f1ocnvd  6063  f1opw2  6067  suppssfv  6069  suppssov1  6070  ofvalg  6082  off  6085  offval2  6088  ofrfval2  6089  caofinvl  6095  mptexw  6104  abrexex  6108  abrexexg  6109  offres  6126  ofmres  6127  op1steq  6170  reldm  6177  mpoexga  6203  mpoexw  6204  mpoex  6205  fnmpoovd  6206  fmpoco  6207  cnvf1o  6216  f1od2  6226  tposssxp  6240  brtpos2  6242  tpos0  6265  iunon  6275  tfrfun  6311  tfr2a  6312  tfrlemisucfn  6315  tfri1d  6326  tfr1onlemsucfn  6331  tfr1onlemubacc  6337  tfr1on  6341  tfri1dALT  6342  tfrcllemubacc  6350  tfrex  6359  rdgfun  6364  rdgon  6377  rdg0  6378  frec0g  6388  frecfnom  6392  freccllem  6393  freccl  6394  frecfcllem  6395  frecfcl  6396  frecsuclem  6397  0lt1o  6431  oafnex  6435  omfnex  6440  fnoei  6443  oeiexg  6444  oeiv  6447  oacl  6451  omcl  6452  oeicl  6453  oav2  6454  omv2  6456  eqer  6557  ecelqsg  6578  elqsn0m  6593  qsel  6602  qliftf  6610  ecoptocl  6612  eroprf  6618  ecopovsym  6621  ecopovtrn  6622  ecopovsymg  6624  ecopovtrng  6625  th3qlem2  6628  th3q  6630  mapsncnv  6685  mapsnf1o3  6687  mptelixpg  6724  ixpsnf1o  6726  en2d  6758  en3d  6759  dom2lem  6762  dom2  6765  1domsn  6809  xpcomen  6817  xpf1o  6834  mapxpen  6838  fidifsnen  6860  isbth  6956  elfir  6962  supsnti  6994  djueq1  7029  djueq2  7030  djuf1olem  7042  inl11  7054  updjud  7071  omp1eom  7084  difinfsn  7089  ctmlemr  7097  ctssdclemn0  7099  ctssdclemr  7101  ctssdc  7102  enumct  7104  infnninf  7112  nnnninf  7114  nnnninfeq  7116  nninfisollemne  7119  nninfisol  7121  ismkvnex  7143  mkvprop  7146  nninfwlporlemd  7160  nninfwlpoimlemginf  7164  exmidonfin  7183  exmidaclem  7197  exmidac  7198  cc3  7242  0npi  7287  indpi  7316  recidnq  7367  addnnnq0  7423  mulnnnq0  7424  genpprecll  7488  genppreclu  7489  caucvgprpr  7686  addsrpr  7719  mulsrpr  7720  0nsr  7723  00sr  7743  caucvgsrlemgt1  7769  opelreal  7801  eqresr  7810  axprecex  7854  nntopi  7868  axpre-suploc  7876  ltxrlt  7997  pncan3  8139  apreim  8534  divcanap2  8609  divcanap3  8627  lble  8875  sup3exmid  8885  nn1gt1  8924  0nn0  9162  pnf0xnn0  9217  0z  9235  decaddm10  9413  decmulnc  9421  10p10e20  9449  4t4e16  9453  5t4e20  9456  6t3e18  9459  6t4e24  9460  6t5e30  9461  7t3e21  9464  7t4e28  9465  7t5e35  9466  7t6e42  9467  7t7e49  9468  8t3e24  9470  8t4e32  9471  8t5e40  9472  8t7e56  9474  8t8e64  9475  9t3e27  9477  9t4e36  9478  9t5e45  9479  9t6e54  9480  9t7e63  9481  9t8e72  9482  9t9e81  9483  infrenegsupex  9565  znq  9595  ltpnf  9749  mnflt  9752  mnfltpnf  9754  xnegpnf  9797  xnegmnf  9798  xaddpnf1  9815  xaddpnf2  9816  xaddmnf1  9817  xaddmnf2  9818  pnfaddmnf  9819  mnfaddpnf  9820  lincmb01cmp  9972  iccf1o  9973  iccen  9975  elfzuz2  9997  fseq1m1p1  10063  fz0tp  10090  fz0to4untppr  10092  flqdiv  10289  frec2uzzd  10368  frec2uzsucd  10369  frecuzrdgrrn  10376  frec2uzrdg  10377  frecuzrdgrcl  10378  frecuzrdgsuc  10382  frecuzrdgrclt  10383  frecuzrdgg  10384  frecuzrdgsuctlem  10391  uzenom  10393  fzfig  10398  nnenom  10402  seqeq1  10416  seq3val  10426  seqvalcd  10427  seqf  10429  seq3p1  10430  seqovcd  10431  seqp1cd  10434  seq3feq2  10438  seq3feq  10440  monoord2  10445  ser3mono  10446  seq3split  10447  seq3caopr2  10450  iseqf1olemqk  10462  seq3f1olemqsumkj  10466  seq3f1olemstep  10469  seq3f1oleml  10471  seq3f1o  10472  seq3homo  10478  seq3z  10479  seqfeq3  10480  seq3distr  10481  ser0f  10483  ser3ge0  10485  ser3le  10486  exp0  10492  0exp  10523  sq0  10578  sq10  10658  sq10e99m1  10659  facnn  10673  fac0  10674  bcval5  10709  hashinfom  10724  hashennn  10726  hashcl  10727  hashfz1  10729  hashen  10730  hash0  10742  fihashdom  10749  hashun  10751  seq3coll  10788  shftfibg  10795  shftfib  10798  shftfn  10799  2shfti  10806  seq3shft  10813  cvg1n  10961  resqrexlemsqa  10999  negfi  11202  xrmaxiflemcom  11223  xrmaxif  11225  infxrnegsupex  11237  climconst2  11265  climres  11277  climshft  11278  serclim0  11279  climle  11308  clim2ser  11311  clim2ser2  11312  climub  11318  climcvg1n  11324  climcaucn  11325  serf0  11326  sumfct  11348  fsum3cvg  11352  summodclem2  11356  zsumdc  11358  fsum3  11361  isumz  11363  fsumf1o  11364  isumss  11365  fsum3cvg2  11368  fsumsersdc  11369  fsum3ser  11371  fsumcl2lem  11372  fsumadd  11380  fsumsplitf  11382  sumsnf  11383  isummulc2  11400  isumadd  11405  fsumcnv  11411  mptfzshft  11416  fsumrev  11417  fsumshft  11418  fsummulc2  11422  iserabs  11449  isumshft  11464  isum1p  11466  isumlessdc  11470  divcnv  11471  trireciplem  11474  trirecip  11475  expcnvap0  11476  expcnvre  11477  expcnv  11478  explecnv  11479  geolim  11485  geolim2  11486  geo2lim  11490  geoisum  11491  geoisumr  11492  geoisum1  11493  geoisum1c  11494  cvgratnnlemseq  11500  cvgratz  11506  mertenslemub  11508  mertenslemi1  11509  mertenslem2  11510  mertensabs  11511  clim2prod  11513  clim2divap  11514  prodfap0  11519  prodfrecap  11520  prodfdivap  11521  prodeq2w  11530  fproddccvg  11546  prodmodclem2  11551  zproddc  11553  fprodseq  11557  fprodntrivap  11558  prod1dc  11560  prodfct  11561  fprodf1o  11562  prodssdc  11563  fprodssdc  11564  fprodmul  11565  prodsnf  11566  fprodshft  11592  fprodrev  11593  fprodcnv  11599  efcllemp  11632  efval  11635  eff  11637  efcvgfsum  11641  reefcl  11642  ege2le3  11645  ef0  11646  efcj  11647  efaddlem  11648  efadd  11649  eftlcl  11662  reeftlcl  11663  eftlub  11664  efsep  11665  effsumlt  11666  efgt1p2  11669  efgt1p  11670  eflegeo  11675  ef01bndlem  11730  sin01bnd  11731  cos01bnd  11732  eirraplem  11750  eirrap  11751  egt2lt3  11753  dvdsmul2  11787  odd2np1lem  11842  nninfdcex  11919  zsupssdc  11920  gcd0val  11926  gcd0id  11945  bezoutlemnewy  11962  nnmindc  12000  nnminle  12001  eucalgcvga  12023  eucalg  12024  lcm0val  12030  qnumdencoprm  12158  qeqnumdivden  12159  phimul  12191  eulerthlemh  12196  eulerthlemth  12197  prmdivdiv  12202  hashgcdeq  12204  phisum  12205  odzval  12206  powm2modprm  12217  reumodprminv  12218  pythagtriplem18  12246  pcpremul  12258  pceulem  12259  pceu  12260  pczpre  12262  pczcl  12263  pcmul  12266  pcdiv  12267  pc1  12270  pczdvds  12278  pczndvds  12280  pczndvds2  12282  pcneg  12289  infpn  12324  1arithlem2  12327  1arith  12330  4sqlem3  12353  mul4sq  12357  xpnnen  12360  ennnfonelemk  12366  ennnfonelemj0  12367  ennnfonelem0  12371  ennnfonelemnn0  12388  ctinfom  12394  ctiunct  12406  ssnnct  12413  nninfdclemcl  12414  nninfdclemf  12415  nninfdclemp1  12416  ressid  12490  2strstr1g  12532  srngstrd  12551  ipsstrd  12573  elrest  12615  elrestr  12616  topnpropgd  12622  mgmsscl  12644  plusffng  12648  mgmplusf  12649  mgmb1mgm1  12651  mgm0  12652  mgm1  12653  opifismgmdc  12654  grpidpropdg  12657  0g0  12659  mgmidcl  12661  mgmlrid  12662  grpidd  12666  sgrpmgm  12677  sgrp0  12679  sgrp1  12680  sgrpidmndm  12685  mndsgrp  12686  mndidcl  12695  mndbn0  12696  hashfinmndnn  12697  ismndd  12702  mndpfo  12703  mndfo  12704  mndpropd  12705  mnd1  12708  mhmf  12717  mhmpropd  12718  mhmlin  12719  mhm0  12720  idmhm  12721  mhmf1o  12722  mndissubm  12726  submss  12727  submid  12728  subm0cl  12729  submcl  12730  0subm  12731  insubm  12732  0mhm  12733  mhmco  12734  mhmima  12735  mhmeql  12736  grpmnd  12744  grppropd  12753  isgrpd2e  12756  dfgrp2  12762  grpbn0  12765  grpn0  12768  grprcan  12770  grpidd2  12774  grpinvval  12776  grpinvfng  12777  grpsubval  12779  grpinvf  12780  grplrinv  12787  grpidinv  12789  grpinvid  12790  grplcan  12791  grpasscan1  12792  grpasscan2  12793  grpinvinv  12796  grpinvcnv  12797  grplmulf1o  12803  grpinvpropdg  12804  grpidssd  12805  grpinvssd  12806  grpinvadd  12807  grpsubf  12808  grpsubrcan  12810  grpinvsub  12811  grpinvval2  12812  grpsubid  12813  grpsubid1  12814  grpsubeq0  12815  grpsubadd0sub  12816  grpsubadd  12817  grpsubsub  12818  grpaddsubass  12819  grppncan  12820  grpnpcan  12821  grpnnncan2  12826  dfgrp3m  12828  grplactcnv  12831  grplactf1o  12832  grpsubpropdg  12833  grpsubpropd2  12834  grp1  12835  grp1inv  12836  mhmid  12838  mhmmnd  12839  mhmfmhm  12840  ghmgrp  12841  mulgfng  12846  mulg0  12847  mulgnn  12848  mulg1  12849  mulgnnp1  12850  mulgnegnn  12852  mulgnn0p1  12853  mulgnnsubcl  12854  mulgnncl  12857  mulgnn0cl  12858  mulgcl  12859  mulgneg  12860  mulgaddcomlem  12864  mulgaddcom  12865  mulginvcom  12866  mulgnn0z  12868  mulgz  12869  mulgnndir  12870  mulgnn0dir  12871  mulgdirlem  12872  mulgdir  12873  mulgneg2  12875  mulgnnass  12876  mulgnn0ass  12877  mulgass  12878  mulgmodid  12880  mulgsubdir  12881  mhmmulg  12882  submmulgcl  12883  cmnpropd  12894  iscmnd  12897  cmnmnd  12900  ablsub2inv  12910  ablsub4  12912  abladdsub4  12913  ablpncan2  12915  ablsubsub4  12918  ablpnpcan  12919  ablnncan  12920  ablsub32  12921  ablnnncan  12922  ablsubsub23  12924  mgpbasg  12930  mgpscag  12931  mgptsetg  12932  mgptopng  12933  mgpdsg  12934  dfur2g  12938  srgcmn  12942  srgmgp  12944  srgdilem  12945  srgcl  12946  srgass  12947  srgideu  12948  srgidcl  12952  srgidmlem  12954  issrgid  12957  srgrz  12960  srglz  12961  srg1zr  12963  srgmulgass  12965  srgpcomp  12966  srgpcompp  12967  srgpcomppsc  12968  srglmhm  12969  srgrmhm  12970  srg1expzeq1  12971  ringgrp  12977  ringmgp  12978  crngring  12984  mgpf  12987  ringdilem  12988  ringcl  12989  crngcom  12990  iscrng2  12991  ringass  12992  ringideu  12993  ringidcl  12996  ringidmlem  12998  isringid  13001  ringid  13002  ringcom  13006  ringabl  13007  ringpropd  13009  crngpropd  13010  isringd  13012  iscrngd  13013  ringlz  13014  ringrz  13015  ringsrg  13016  ring1eq0  13017  ringnegl  13020  rngnegr  13021  ringmneg1  13022  ringmneg2  13023  ringsubdi  13025  rngsubdir  13026  mulgass2  13027  ring1  13028  ringn0  13029  toptopon2  13068  toponmax  13074  tpstop  13084  tpspropd  13085  tsettps  13087  eltpsg  13089  tgiun  13124  ntrval  13161  clsval  13162  0cld  13163  uncld  13164  cldcls  13165  ntr0  13185  isopn3i  13186  neif  13192  neival  13194  neii2  13200  neiss  13201  opnneiss  13209  innei  13214  neissex  13216  tgrest  13220  stoig  13224  restco  13225  resttopon2  13229  restopn2  13234  cnpval  13249  cntop1  13252  cntop2  13253  cnprcl2k  13257  lmcvg  13268  iscnp4  13269  cnima  13271  cnco  13272  cnclima  13274  cnntri  13275  cnntr  13276  cnss1  13277  cnss2  13278  cncnpi  13279  cncnp  13281  cnrest  13286  cnrest2  13287  cnrest2r  13288  lmss  13297  lmres  13299  lmcn  13302  txuni2  13307  txbasex  13308  eltx  13310  txtop  13311  txtopon  13313  txopn  13316  txss12  13317  txbasval  13318  neitx  13319  txcnp  13322  upxp  13323  txcnmpt  13324  uptx  13325  txcn  13326  txrest  13327  txdis1cn  13329  txlm  13330  lmcn2  13331  cnmpt11  13334  cnmpt11f  13335  cnmpt1t  13336  cnmpt12  13338  cnmpt21  13342  cnmpt21f  13343  cnmpt2t  13344  cnmpt22  13345  cnmpt1res  13347  cnmpt2res  13348  cnmptcom  13349  imasnopn  13350  hmeocnv  13358  hmeoopn  13362  hmeocld  13363  hmeontr  13364  hmeoimaf1o  13365  hmeores  13366  txhmeo  13370  txswaphmeo  13372  xmet0  13414  blfvalps  13436  blfps  13460  blf  13461  blpnfctr  13490  xmetresbl  13491  isxms2  13503  xmstps  13508  msxms  13509  xmsxmet  13511  msmet  13512  xmspropd  13528  mspropd  13529  neibl  13542  bdxmet  13552  bdmopn  13555  mopnex  13556  xmetxp  13558  xmettxlem  13560  xmettx  13561  txmetcnp  13569  metcnpd  13571  cnmet  13581  unicntopcntop  13587  cnopncntop  13588  remetdval  13590  resubmet  13599  tgioo2cntop  13600  addcncntoplem  13602  divcnap  13606  fsumcncntop  13607  divccncfap  13628  cncfmet  13630  cncfcncntop  13631  cncfmptc  13633  cncfmptid  13634  cncfmpt1f  13635  cncfmpt2fcntop  13636  cdivcncfap  13638  negfcncf  13640  mulcncflem  13641  mulcncf  13642  cnopnap  13645  ivthinc  13672  ivthdec  13673  limcmpted  13683  limcimolemlt  13684  cnplimcim  13687  cnplimclemr  13689  cnlimcim  13691  cnlimc  13692  cnmptlimc  13694  limccnpcntop  13695  limccnp2lem  13696  limccnp2cntop  13697  reldvg  13699  dvfvalap  13701  dvcl  13703  dvbss  13705  dvfgg  13708  dvidlemap  13711  dvcnp2cntop  13714  dvcn  13715  dvaddxxbr  13716  dvmulxxbr  13717  dvaddxx  13718  dvmulxx  13719  dviaddf  13720  dvimulf  13721  dvcoapbr  13722  dvcjbr  13723  dvrecap  13728  dveflem  13738  dvef  13739  sincn  13741  coscn  13742  lgsfcl  13960  lgsfle1  13961  lgsval4lem  13963  lgscl2  13964  lgs0  13965  lgscl  13966  lgsle1  13967  lgsval2  13968  lgs2  13969  lgsval4  13972  lgsfcl3  13973  lgsneg  13976  lgsmod  13978  lgsdirprm  13986  lgsdir  13987  lgsdi  13989  lgsne0  13990  2sqlem9  14011  ex-or  14014  ex-an  14015  1kp2ke3k  14016  ex-exp  14019  ex-fac  14020  fnmptd  14096  bj-2inf  14230  bj-inf2vnlem1  14262  subctctexmid  14291  nnsf  14295  peano3nninf  14297  nninfself  14303  nninfsellemeqinf  14306  nninffeq  14310  iooreen  14324  trilpolemcl  14326  trilpolemisumle  14327  trilpolemeq1  14329  trilpolemlt1  14330  iswomni0  14340  dceqnconst  14348  dcapnconst  14349  nconstwlpolemgt0  14352