Theorem eqid 2165

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 170	. 2 |- ( x e. A <-> x e. A )
2	1	eqriv 2162	1 |- A = A

Syntax hints:   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  eqidd  2166  neirr  2344  sbsbc  2954  sbceqal  3005  dfnul2  3410  snidg  3604  prid1g  3679  tpid1  3686  tpid1g  3687  tpid2  3688  tpid2g  3689  tpid3  3691  dfiin2g  3898  eqbrtrid  4016  eqbrtrrid  4017  breqtrdi  4022  opabbii  4048  mpteq2ia  4067  mpteq2da  4070  sucidg  4393  onsucelsucexmidlem1  4504  regexmidlemm  4508  regexmidlem1  4509  reg2exmidlema  4510  regexmid  4511  reg2exmid  4512  reg3exmid  4556  tfisi  4563  finds1  4578  nn0suc  4580  nndceq0  4594  0elnn  4595  nnregexmid  4597  opelxp  4633  relopab  4730  relop  4753  ididg  4756  elrnmpt1s  4853  dfiun3g  4860  dfiin3g  4861  dmmptg  5100  funfn  5217  mpt0  5314  f0  5377  dffn4  5415  f1orn  5441  f1oabexg  5443  f1o00  5466  f1o0  5468  fnbrfvb  5526  fnrnfv  5532  funfvdm  5548  fvmptg  5561  fvmptd  5566  fvmpt2d  5571  fvmptdf  5572  mpteqb  5575  fvmptt  5576  funfvop  5596  eldmrexrn  5625  fvmptelrn  5637  fmpttd  5639  fmpt2d  5646  fmptco  5650  fmptcof  5651  fnasrn  5662  fnasrng  5664  mptexg  5709  eufnfv  5714  idref  5724  f1elima  5740  fliftrel  5759  fliftel  5760  fliftel1  5761  fliftcnv  5762  fliftf  5766  riotabiia  5814  acexmidlem2  5838  acexmidlemv  5839  oprabbii  5893  mpoeq12  5898  ovmpodxf  5963  ovmpodf  5969  ov6g  5975  f1ocnvd  6039  f1opw2  6043  suppssfv  6045  suppssov1  6046  ofvalg  6058  off  6061  offval2  6064  ofrfval2  6065  caofinvl  6071  abrexex  6082  abrexexg  6083  offres  6100  ofmres  6101  op1steq  6144  reldm  6151  mpoexga  6177  mpoex  6178  fnmpoovd  6179  fmpoco  6180  cnvf1o  6189  f1od2  6199  tposssxp  6213  brtpos2  6215  tpos0  6238  iunon  6248  tfrfun  6284  tfr2a  6285  tfrlemisucfn  6288  tfri1d  6299  tfr1onlemsucfn  6304  tfr1onlemubacc  6310  tfr1on  6314  tfri1dALT  6315  tfrcllemubacc  6323  tfrex  6332  rdgfun  6337  rdgon  6350  rdg0  6351  frec0g  6361  frecfnom  6365  freccllem  6366  freccl  6367  frecfcllem  6368  frecfcl  6369  frecsuclem  6370  0lt1o  6404  oafnex  6408  omfnex  6413  fnoei  6416  oeiexg  6417  oeiv  6420  oacl  6424  omcl  6425  oeicl  6426  oav2  6427  omv2  6429  eqer  6529  ecelqsg  6550  elqsn0m  6565  qsel  6574  qliftf  6582  ecoptocl  6584  eroprf  6590  ecopovsym  6593  ecopovtrn  6594  ecopovsymg  6596  ecopovtrng  6597  th3qlem2  6600  th3q  6602  mapsncnv  6657  mapsnf1o3  6659  mptelixpg  6696  ixpsnf1o  6698  en2d  6730  en3d  6731  dom2lem  6734  dom2  6737  1domsn  6781  xpcomen  6789  xpf1o  6806  mapxpen  6810  fidifsnen  6832  isbth  6928  elfir  6934  supsnti  6966  djueq1  7001  djueq2  7002  djuf1olem  7014  inl11  7026  updjud  7043  omp1eom  7056  difinfsn  7061  ctmlemr  7069  ctssdclemn0  7071  ctssdclemr  7073  ctssdc  7074  enumct  7076  infnninf  7084  nnnninf  7086  nnnninfeq  7088  nninfisollemne  7091  nninfisol  7093  ismkvnex  7115  mkvprop  7118  exmidonfin  7146  exmidaclem  7160  exmidac  7161  cc3  7205  0npi  7250  indpi  7279  recidnq  7330  addnnnq0  7386  mulnnnq0  7387  genpprecll  7451  genppreclu  7452  caucvgprpr  7649  addsrpr  7682  mulsrpr  7683  0nsr  7686  00sr  7706  caucvgsrlemgt1  7732  opelreal  7764  eqresr  7773  axprecex  7817  nntopi  7831  axpre-suploc  7839  ltxrlt  7960  pncan3  8102  apreim  8497  divcanap2  8572  divcanap3  8590  lble  8838  sup3exmid  8848  nn1gt1  8887  0nn0  9125  pnf0xnn0  9180  0z  9198  decaddm10  9376  decmulnc  9384  10p10e20  9412  4t4e16  9416  5t4e20  9419  6t3e18  9422  6t4e24  9423  6t5e30  9424  7t3e21  9427  7t4e28  9428  7t5e35  9429  7t6e42  9430  7t7e49  9431  8t3e24  9433  8t4e32  9434  8t5e40  9435  8t7e56  9437  8t8e64  9438  9t3e27  9440  9t4e36  9441  9t5e45  9442  9t6e54  9443  9t7e63  9444  9t8e72  9445  9t9e81  9446  infrenegsupex  9528  znq  9558  ltpnf  9712  mnflt  9715  mnfltpnf  9717  xnegpnf  9760  xnegmnf  9761  xaddpnf1  9778  xaddpnf2  9779  xaddmnf1  9780  xaddmnf2  9781  pnfaddmnf  9782  mnfaddpnf  9783  lincmb01cmp  9935  iccf1o  9936  iccen  9938  elfzuz2  9960  fseq1m1p1  10026  fz0tp  10053  fz0to4untppr  10055  flqdiv  10252  frec2uzzd  10331  frec2uzsucd  10332  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  frecuzrdgsuctlem  10354  uzenom  10356  fzfig  10361  nnenom  10365  seqeq1  10379  seq3val  10389  seqvalcd  10390  seqf  10392  seq3p1  10393  seqovcd  10394  seqp1cd  10397  seq3feq2  10401  seq3feq  10403  monoord2  10408  ser3mono  10409  seq3split  10410  seq3caopr2  10413  iseqf1olemqk  10425  seq3f1olemqsumkj  10429  seq3f1olemstep  10432  seq3f1oleml  10434  seq3f1o  10435  seq3homo  10441  seq3z  10442  seqfeq3  10443  seq3distr  10444  ser0f  10446  ser3ge0  10448  ser3le  10449  exp0  10455  0exp  10486  sq0  10541  sq10  10621  sq10e99m1  10622  facnn  10636  fac0  10637  bcval5  10672  hashinfom  10687  hashennn  10689  hashcl  10690  hashfz1  10692  hashen  10693  hash0  10706  fihashdom  10712  hashun  10714  seq3coll  10751  shftfibg  10758  shftfib  10761  shftfn  10762  2shfti  10769  seq3shft  10776  cvg1n  10924  resqrexlemsqa  10962  negfi  11165  xrmaxiflemcom  11186  xrmaxif  11188  infxrnegsupex  11200  climconst2  11228  climres  11240  climshft  11241  serclim0  11242  climle  11271  clim2ser  11274  clim2ser2  11275  climub  11281  climcvg1n  11287  climcaucn  11288  serf0  11289  sumfct  11311  fsum3cvg  11315  summodclem2  11319  zsumdc  11321  fsum3  11324  isumz  11326  fsumf1o  11327  isumss  11328  fsum3cvg2  11331  fsumsersdc  11332  fsum3ser  11334  fsumcl2lem  11335  fsumadd  11343  fsumsplitf  11345  sumsnf  11346  isummulc2  11363  isumadd  11368  fsumcnv  11374  mptfzshft  11379  fsumrev  11380  fsumshft  11381  fsummulc2  11385  iserabs  11412  isumshft  11427  isum1p  11429  isumlessdc  11433  divcnv  11434  trireciplem  11437  trirecip  11438  expcnvap0  11439  expcnvre  11440  expcnv  11441  explecnv  11442  geolim  11448  geolim2  11449  geo2lim  11453  geoisum  11454  geoisumr  11455  geoisum1  11456  geoisum1c  11457  cvgratnnlemseq  11463  cvgratz  11469  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  clim2prod  11476  clim2divap  11477  prodfap0  11482  prodfrecap  11483  prodfdivap  11484  prodeq2w  11493  fproddccvg  11509  prodmodclem2  11514  zproddc  11516  fprodseq  11520  fprodntrivap  11521  prod1dc  11523  prodfct  11524  fprodf1o  11525  prodssdc  11526  fprodssdc  11527  fprodmul  11528  prodsnf  11529  fprodshft  11555  fprodrev  11556  fprodcnv  11562  efcllemp  11595  efval  11598  eff  11600  efcvgfsum  11604  reefcl  11605  ege2le3  11608  ef0  11609  efcj  11610  efaddlem  11611  efadd  11612  eftlcl  11625  reeftlcl  11626  eftlub  11627  efsep  11628  effsumlt  11629  efgt1p2  11632  efgt1p  11633  eflegeo  11638  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  eirraplem  11713  eirrap  11714  egt2lt3  11716  dvdsmul2  11750  odd2np1lem  11805  nninfdcex  11882  zsupssdc  11883  gcd0val  11889  gcd0id  11908  bezoutlemnewy  11925  nnmindc  11963  nnminle  11964  eucalgcvga  11986  eucalg  11987  lcm0val  11993  qnumdencoprm  12121  qeqnumdivden  12122  phimul  12154  eulerthlemh  12159  eulerthlemth  12160  prmdivdiv  12165  hashgcdeq  12167  phisum  12168  odzval  12169  powm2modprm  12180  reumodprminv  12181  pythagtriplem18  12209  pcpremul  12221  pceulem  12222  pceu  12223  pczpre  12225  pczcl  12226  pcmul  12229  pcdiv  12230  pc1  12233  pczdvds  12241  pczndvds  12243  pczndvds2  12245  pcneg  12252  infpn  12287  1arithlem2  12290  1arith  12293  4sqlem3  12316  mul4sq  12320  xpnnen  12323  ennnfonelemk  12329  ennnfonelemj0  12330  ennnfonelem0  12334  ennnfonelemnn0  12351  ctinfom  12357  ctiunct  12369  ssnnct  12376  nninfdclemcl  12377  nninfdclemf  12378  nninfdclemp1  12379  ressid  12451  2strstr1g  12493  srngstrd  12512  ipsstrd  12531  elrest  12558  elrestr  12559  topnpropgd  12565  toptopon2  12617  toponmax  12623  tpstop  12633  tpspropd  12634  tsettps  12636  eltpsg  12638  tgiun  12673  ntrval  12710  clsval  12711  0cld  12712  uncld  12713  cldcls  12714  ntr0  12734  isopn3i  12735  neif  12741  neival  12743  neii2  12749  neiss  12750  opnneiss  12758  innei  12763  neissex  12765  tgrest  12769  stoig  12773  restco  12774  resttopon2  12778  restopn2  12783  cnpval  12798  cntop1  12801  cntop2  12802  cnprcl2k  12806  lmcvg  12817  iscnp4  12818  cnima  12820  cnco  12821  cnclima  12823  cnntri  12824  cnntr  12825  cnss1  12826  cnss2  12827  cncnpi  12828  cncnp  12830  cnrest  12835  cnrest2  12836  cnrest2r  12837  lmss  12846  lmres  12848  lmcn  12851  txuni2  12856  txbasex  12857  eltx  12859  txtop  12860  txtopon  12862  txopn  12865  txss12  12866  txbasval  12867  neitx  12868  txcnp  12871  upxp  12872  txcnmpt  12873  uptx  12874  txcn  12875  txrest  12876  txdis1cn  12878  txlm  12879  lmcn2  12880  cnmpt11  12883  cnmpt11f  12884  cnmpt1t  12885  cnmpt12  12887  cnmpt21  12891  cnmpt21f  12892  cnmpt2t  12893  cnmpt22  12894  cnmpt1res  12896  cnmpt2res  12897  cnmptcom  12898  imasnopn  12899  hmeocnv  12907  hmeoopn  12911  hmeocld  12912  hmeontr  12913  hmeoimaf1o  12914  hmeores  12915  txhmeo  12919  txswaphmeo  12921  xmet0  12963  blfvalps  12985  blfps  13009  blf  13010  blpnfctr  13039  xmetresbl  13040  isxms2  13052  xmstps  13057  msxms  13058  xmsxmet  13060  msmet  13061  xmspropd  13077  mspropd  13078  neibl  13091  bdxmet  13101  bdmopn  13104  mopnex  13105  xmetxp  13107  xmettxlem  13109  xmettx  13110  txmetcnp  13118  metcnpd  13120  cnmet  13130  unicntopcntop  13136  cnopncntop  13137  remetdval  13139  resubmet  13148  tgioo2cntop  13149  addcncntoplem  13151  divcnap  13155  fsumcncntop  13156  divccncfap  13177  cncfmet  13179  cncfcncntop  13180  cncfmptc  13182  cncfmptid  13183  cncfmpt1f  13184  cncfmpt2fcntop  13185  cdivcncfap  13187  negfcncf  13189  mulcncflem  13190  mulcncf  13191  cnopnap  13194  ivthinc  13221  ivthdec  13222  limcmpted  13232  limcimolemlt  13233  cnplimcim  13236  cnplimclemr  13238  cnlimcim  13240  cnlimc  13241  cnmptlimc  13243  limccnpcntop  13244  limccnp2lem  13245  limccnp2cntop  13246  reldvg  13248  dvfvalap  13250  dvcl  13252  dvbss  13254  dvfgg  13257  dvidlemap  13260  dvcnp2cntop  13263  dvcn  13264  dvaddxxbr  13265  dvmulxxbr  13266  dvaddxx  13267  dvmulxx  13268  dviaddf  13269  dvimulf  13270  dvcoapbr  13271  dvcjbr  13272  dvrecap  13277  dveflem  13287  dvef  13288  sincn  13290  coscn  13291  lgsfcl  13509  lgsfle1  13510  lgsval4lem  13512  lgscl2  13513  lgs0  13514  lgscl  13515  lgsle1  13516  lgsval2  13517  lgs2  13518  lgsval4  13521  lgsfcl3  13522  lgsneg  13525  lgsmod  13527  lgsdirprm  13535  lgsdir  13536  lgsdi  13538  lgsne0  13539  2sqlem9  13560  ex-or  13563  ex-an  13564  1kp2ke3k  13565  ex-exp  13568  ex-fac  13569  fnmptd  13646  bj-2inf  13780  bj-inf2vnlem1  13812  subctctexmid  13841  nnsf  13845  peano3nninf  13847  nninfself  13853  nninfsellemeqinf  13856  nninffeq  13860  iooreen  13874  trilpolemcl  13876  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  iswomni0  13890  dceqnconst  13898  dcapnconst  13899  nconstwlpolemgt0  13902