Theorem eqid 2170

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

Syntax hints:   = wceq 1348   e. wcel 2141

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 1442  ax-ext 2152

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

This theorem is referenced by:  eqidd  2171  neirr  2349  sbsbc  2959  sbceqal  3010  dfnul2  3416  snidg  3612  prid1g  3687  tpid1  3694  tpid1g  3695  tpid2  3696  tpid2g  3697  tpid3  3699  dfiin2g  3906  eqbrtrid  4024  eqbrtrrid  4025  breqtrdi  4030  opabbii  4056  mpteq2ia  4075  mpteq2da  4078  sucidg  4401  onsucelsucexmidlem1  4512  regexmidlemm  4516  regexmidlem1  4517  reg2exmidlema  4518  regexmid  4519  reg2exmid  4520  reg3exmid  4564  tfisi  4571  finds1  4586  nn0suc  4588  nndceq0  4602  0elnn  4603  nnregexmid  4605  opelxp  4641  relopab  4738  relop  4761  ididg  4764  elrnmpt1s  4861  dfiun3g  4868  dfiin3g  4869  dmmptg  5108  funfn  5228  mpt0  5325  f0  5388  dffn4  5426  f1orn  5452  f1oabexg  5454  f1o00  5477  f1o0  5479  fnbrfvb  5537  fnrnfv  5543  funfvdm  5559  fvmptg  5572  fvmptd  5577  fvmpt2d  5582  fvmptdf  5583  mpteqb  5586  fvmptt  5587  fnmptfvd  5600  funfvop  5608  eldmrexrn  5637  fvmptelrn  5649  fmpttd  5651  fmpt2d  5658  fmptco  5662  fmptcof  5663  fnasrn  5674  fnasrng  5676  mptexg  5721  eufnfv  5726  idref  5736  f1elima  5752  fliftrel  5771  fliftel  5772  fliftel1  5773  fliftcnv  5774  fliftf  5778  riotabiia  5826  acexmidlem2  5850  acexmidlemv  5851  oprabbii  5908  mpoeq12  5913  ovmpodxf  5978  ovmpodf  5984  ov6g  5990  f1ocnvd  6051  f1opw2  6055  suppssfv  6057  suppssov1  6058  ofvalg  6070  off  6073  offval2  6076  ofrfval2  6077  caofinvl  6083  mptexw  6092  abrexex  6096  abrexexg  6097  offres  6114  ofmres  6115  op1steq  6158  reldm  6165  mpoexga  6191  mpoexw  6192  mpoex  6193  fnmpoovd  6194  fmpoco  6195  cnvf1o  6204  f1od2  6214  tposssxp  6228  brtpos2  6230  tpos0  6253  iunon  6263  tfrfun  6299  tfr2a  6300  tfrlemisucfn  6303  tfri1d  6314  tfr1onlemsucfn  6319  tfr1onlemubacc  6325  tfr1on  6329  tfri1dALT  6330  tfrcllemubacc  6338  tfrex  6347  rdgfun  6352  rdgon  6365  rdg0  6366  frec0g  6376  frecfnom  6380  freccllem  6381  freccl  6382  frecfcllem  6383  frecfcl  6384  frecsuclem  6385  0lt1o  6419  oafnex  6423  omfnex  6428  fnoei  6431  oeiexg  6432  oeiv  6435  oacl  6439  omcl  6440  oeicl  6441  oav2  6442  omv2  6444  eqer  6545  ecelqsg  6566  elqsn0m  6581  qsel  6590  qliftf  6598  ecoptocl  6600  eroprf  6606  ecopovsym  6609  ecopovtrn  6610  ecopovsymg  6612  ecopovtrng  6613  th3qlem2  6616  th3q  6618  mapsncnv  6673  mapsnf1o3  6675  mptelixpg  6712  ixpsnf1o  6714  en2d  6746  en3d  6747  dom2lem  6750  dom2  6753  1domsn  6797  xpcomen  6805  xpf1o  6822  mapxpen  6826  fidifsnen  6848  isbth  6944  elfir  6950  supsnti  6982  djueq1  7017  djueq2  7018  djuf1olem  7030  inl11  7042  updjud  7059  omp1eom  7072  difinfsn  7077  ctmlemr  7085  ctssdclemn0  7087  ctssdclemr  7089  ctssdc  7090  enumct  7092  infnninf  7100  nnnninf  7102  nnnninfeq  7104  nninfisollemne  7107  nninfisol  7109  ismkvnex  7131  mkvprop  7134  nninfwlporlemd  7148  nninfwlpoimlemginf  7152  exmidonfin  7171  exmidaclem  7185  exmidac  7186  cc3  7230  0npi  7275  indpi  7304  recidnq  7355  addnnnq0  7411  mulnnnq0  7412  genpprecll  7476  genppreclu  7477  caucvgprpr  7674  addsrpr  7707  mulsrpr  7708  0nsr  7711  00sr  7731  caucvgsrlemgt1  7757  opelreal  7789  eqresr  7798  axprecex  7842  nntopi  7856  axpre-suploc  7864  ltxrlt  7985  pncan3  8127  apreim  8522  divcanap2  8597  divcanap3  8615  lble  8863  sup3exmid  8873  nn1gt1  8912  0nn0  9150  pnf0xnn0  9205  0z  9223  decaddm10  9401  decmulnc  9409  10p10e20  9437  4t4e16  9441  5t4e20  9444  6t3e18  9447  6t4e24  9448  6t5e30  9449  7t3e21  9452  7t4e28  9453  7t5e35  9454  7t6e42  9455  7t7e49  9456  8t3e24  9458  8t4e32  9459  8t5e40  9460  8t7e56  9462  8t8e64  9463  9t3e27  9465  9t4e36  9466  9t5e45  9467  9t6e54  9468  9t7e63  9469  9t8e72  9470  9t9e81  9471  infrenegsupex  9553  znq  9583  ltpnf  9737  mnflt  9740  mnfltpnf  9742  xnegpnf  9785  xnegmnf  9786  xaddpnf1  9803  xaddpnf2  9804  xaddmnf1  9805  xaddmnf2  9806  pnfaddmnf  9807  mnfaddpnf  9808  lincmb01cmp  9960  iccf1o  9961  iccen  9963  elfzuz2  9985  fseq1m1p1  10051  fz0tp  10078  fz0to4untppr  10080  flqdiv  10277  frec2uzzd  10356  frec2uzsucd  10357  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgsuctlem  10379  uzenom  10381  fzfig  10386  nnenom  10390  seqeq1  10404  seq3val  10414  seqvalcd  10415  seqf  10417  seq3p1  10418  seqovcd  10419  seqp1cd  10422  seq3feq2  10426  seq3feq  10428  monoord2  10433  ser3mono  10434  seq3split  10435  seq3caopr2  10438  iseqf1olemqk  10450  seq3f1olemqsumkj  10454  seq3f1olemstep  10457  seq3f1oleml  10459  seq3f1o  10460  seq3homo  10466  seq3z  10467  seqfeq3  10468  seq3distr  10469  ser0f  10471  ser3ge0  10473  ser3le  10474  exp0  10480  0exp  10511  sq0  10566  sq10  10646  sq10e99m1  10647  facnn  10661  fac0  10662  bcval5  10697  hashinfom  10712  hashennn  10714  hashcl  10715  hashfz1  10717  hashen  10718  hash0  10731  fihashdom  10738  hashun  10740  seq3coll  10777  shftfibg  10784  shftfib  10787  shftfn  10788  2shfti  10795  seq3shft  10802  cvg1n  10950  resqrexlemsqa  10988  negfi  11191  xrmaxiflemcom  11212  xrmaxif  11214  infxrnegsupex  11226  climconst2  11254  climres  11266  climshft  11267  serclim0  11268  climle  11297  clim2ser  11300  clim2ser2  11301  climub  11307  climcvg1n  11313  climcaucn  11314  serf0  11315  sumfct  11337  fsum3cvg  11341  summodclem2  11345  zsumdc  11347  fsum3  11350  isumz  11352  fsumf1o  11353  isumss  11354  fsum3cvg2  11357  fsumsersdc  11358  fsum3ser  11360  fsumcl2lem  11361  fsumadd  11369  fsumsplitf  11371  sumsnf  11372  isummulc2  11389  isumadd  11394  fsumcnv  11400  mptfzshft  11405  fsumrev  11406  fsumshft  11407  fsummulc2  11411  iserabs  11438  isumshft  11453  isum1p  11455  isumlessdc  11459  divcnv  11460  trireciplem  11463  trirecip  11464  expcnvap0  11465  expcnvre  11466  expcnv  11467  explecnv  11468  geolim  11474  geolim2  11475  geo2lim  11479  geoisum  11480  geoisumr  11481  geoisum1  11482  geoisum1c  11483  cvgratnnlemseq  11489  cvgratz  11495  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  clim2prod  11502  clim2divap  11503  prodfap0  11508  prodfrecap  11509  prodfdivap  11510  prodeq2w  11519  fproddccvg  11535  prodmodclem2  11540  zproddc  11542  fprodseq  11546  fprodntrivap  11547  prod1dc  11549  prodfct  11550  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  fprodmul  11554  prodsnf  11555  fprodshft  11581  fprodrev  11582  fprodcnv  11588  efcllemp  11621  efval  11624  eff  11626  efcvgfsum  11630  reefcl  11631  ege2le3  11634  ef0  11635  efcj  11636  efaddlem  11637  efadd  11638  eftlcl  11651  reeftlcl  11652  eftlub  11653  efsep  11654  effsumlt  11655  efgt1p2  11658  efgt1p  11659  eflegeo  11664  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  eirraplem  11739  eirrap  11740  egt2lt3  11742  dvdsmul2  11776  odd2np1lem  11831  nninfdcex  11908  zsupssdc  11909  gcd0val  11915  gcd0id  11934  bezoutlemnewy  11951  nnmindc  11989  nnminle  11990  eucalgcvga  12012  eucalg  12013  lcm0val  12019  qnumdencoprm  12147  qeqnumdivden  12148  phimul  12180  eulerthlemh  12185  eulerthlemth  12186  prmdivdiv  12191  hashgcdeq  12193  phisum  12194  odzval  12195  powm2modprm  12206  reumodprminv  12207  pythagtriplem18  12235  pcpremul  12247  pceulem  12248  pceu  12249  pczpre  12251  pczcl  12252  pcmul  12255  pcdiv  12256  pc1  12259  pczdvds  12267  pczndvds  12269  pczndvds2  12271  pcneg  12278  infpn  12313  1arithlem2  12316  1arith  12319  4sqlem3  12342  mul4sq  12346  xpnnen  12349  ennnfonelemk  12355  ennnfonelemj0  12356  ennnfonelem0  12360  ennnfonelemnn0  12377  ctinfom  12383  ctiunct  12395  ssnnct  12402  nninfdclemcl  12403  nninfdclemf  12404  nninfdclemp1  12405  ressid  12479  2strstr1g  12521  srngstrd  12540  ipsstrd  12559  elrest  12586  elrestr  12587  topnpropgd  12593  mgmsscl  12615  plusffng  12619  mgmplusf  12620  mgmb1mgm1  12622  mgm0  12623  mgm1  12624  opifismgmdc  12625  grpidpropdg  12628  0g0  12630  mgmidcl  12632  mgmlrid  12633  grpidd  12637  sgrpmgm  12648  sgrp0  12650  sgrp1  12651  sgrpidmndm  12656  mndsgrp  12657  mndidcl  12666  mndbn0  12667  hashfinmndnn  12668  ismndd  12673  mndpfo  12674  mndfo  12675  mndpropd  12676  mnd1  12679  mhmf  12688  mhmpropd  12689  mhmlin  12690  mhm0  12691  idmhm  12692  mhmf1o  12693  mndissubm  12697  submss  12698  submid  12699  subm0cl  12700  submcl  12701  0subm  12702  insubm  12703  0mhm  12704  mhmco  12705  mhmima  12706  mhmeql  12707  grpmnd  12715  grppropd  12724  isgrpd2e  12726  dfgrp2  12732  grpbn0  12735  grpn0  12738  grprcan  12740  grpidd2  12744  grpinvval  12746  grpinvfng  12747  grpsubval  12749  grpinvf  12750  grplrinv  12757  grpidinv  12759  grpinvid  12760  grplcan  12761  grpasscan1  12762  grpasscan2  12763  grpinvinv  12766  grpinvcnv  12767  toptopon2  12811  toponmax  12817  tpstop  12827  tpspropd  12828  tsettps  12830  eltpsg  12832  tgiun  12867  ntrval  12904  clsval  12905  0cld  12906  uncld  12907  cldcls  12908  ntr0  12928  isopn3i  12929  neif  12935  neival  12937  neii2  12943  neiss  12944  opnneiss  12952  innei  12957  neissex  12959  tgrest  12963  stoig  12967  restco  12968  resttopon2  12972  restopn2  12977  cnpval  12992  cntop1  12995  cntop2  12996  cnprcl2k  13000  lmcvg  13011  iscnp4  13012  cnima  13014  cnco  13015  cnclima  13017  cnntri  13018  cnntr  13019  cnss1  13020  cnss2  13021  cncnpi  13022  cncnp  13024  cnrest  13029  cnrest2  13030  cnrest2r  13031  lmss  13040  lmres  13042  lmcn  13045  txuni2  13050  txbasex  13051  eltx  13053  txtop  13054  txtopon  13056  txopn  13059  txss12  13060  txbasval  13061  neitx  13062  txcnp  13065  upxp  13066  txcnmpt  13067  uptx  13068  txcn  13069  txrest  13070  txdis1cn  13072  txlm  13073  lmcn2  13074  cnmpt11  13077  cnmpt11f  13078  cnmpt1t  13079  cnmpt12  13081  cnmpt21  13085  cnmpt21f  13086  cnmpt2t  13087  cnmpt22  13088  cnmpt1res  13090  cnmpt2res  13091  cnmptcom  13092  imasnopn  13093  hmeocnv  13101  hmeoopn  13105  hmeocld  13106  hmeontr  13107  hmeoimaf1o  13108  hmeores  13109  txhmeo  13113  txswaphmeo  13115  xmet0  13157  blfvalps  13179  blfps  13203  blf  13204  blpnfctr  13233  xmetresbl  13234  isxms2  13246  xmstps  13251  msxms  13252  xmsxmet  13254  msmet  13255  xmspropd  13271  mspropd  13272  neibl  13285  bdxmet  13295  bdmopn  13298  mopnex  13299  xmetxp  13301  xmettxlem  13303  xmettx  13304  txmetcnp  13312  metcnpd  13314  cnmet  13324  unicntopcntop  13330  cnopncntop  13331  remetdval  13333  resubmet  13342  tgioo2cntop  13343  addcncntoplem  13345  divcnap  13349  fsumcncntop  13350  divccncfap  13371  cncfmet  13373  cncfcncntop  13374  cncfmptc  13376  cncfmptid  13377  cncfmpt1f  13378  cncfmpt2fcntop  13379  cdivcncfap  13381  negfcncf  13383  mulcncflem  13384  mulcncf  13385  cnopnap  13388  ivthinc  13415  ivthdec  13416  limcmpted  13426  limcimolemlt  13427  cnplimcim  13430  cnplimclemr  13432  cnlimcim  13434  cnlimc  13435  cnmptlimc  13437  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  reldvg  13442  dvfvalap  13444  dvcl  13446  dvbss  13448  dvfgg  13451  dvidlemap  13454  dvcnp2cntop  13457  dvcn  13458  dvaddxxbr  13459  dvmulxxbr  13460  dvaddxx  13461  dvmulxx  13462  dviaddf  13463  dvimulf  13464  dvcoapbr  13465  dvcjbr  13466  dvrecap  13471  dveflem  13481  dvef  13482  sincn  13484  coscn  13485  lgsfcl  13703  lgsfle1  13704  lgsval4lem  13706  lgscl2  13707  lgs0  13708  lgscl  13709  lgsle1  13710  lgsval2  13711  lgs2  13712  lgsval4  13715  lgsfcl3  13716  lgsneg  13719  lgsmod  13721  lgsdirprm  13729  lgsdir  13730  lgsdi  13732  lgsne0  13733  2sqlem9  13754  ex-or  13757  ex-an  13758  1kp2ke3k  13759  ex-exp  13762  ex-fac  13763  fnmptd  13839  bj-2inf  13973  bj-inf2vnlem1  14005  subctctexmid  14034  nnsf  14038  peano3nninf  14040  nninfself  14046  nninfsellemeqinf  14049  nninffeq  14053  iooreen  14067  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  iswomni0  14083  dceqnconst  14091  dcapnconst  14092  nconstwlpolemgt0  14095