Theorem eqid 2140

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

Syntax hints:   = wceq 1332   e. wcel 1481

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 1426  ax-ext 2122

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

This theorem is referenced by:  eqidd  2141  neirr  2318  sbsbc  2917  sbceqal  2968  dfnul2  3370  snidg  3561  prid1g  3635  tpid1  3642  tpid1g  3643  tpid2  3644  tpid2g  3645  tpid3  3647  dfiin2g  3854  eqbrtrid  3971  eqbrtrrid  3972  breqtrdi  3977  opabbii  4003  mpteq2ia  4022  mpteq2da  4025  sucidg  4346  onsucelsucexmidlem1  4451  regexmidlemm  4455  regexmidlem1  4456  reg2exmidlema  4457  regexmid  4458  reg2exmid  4459  reg3exmid  4502  tfisi  4509  finds1  4524  nn0suc  4526  nndceq0  4539  0elnn  4540  nnregexmid  4542  opelxp  4577  relopab  4674  relop  4697  ididg  4700  elrnmpt1s  4797  dfiun3g  4804  dfiin3g  4805  dmmptg  5044  funfn  5161  mpt0  5258  f0  5321  dffn4  5359  f1orn  5385  f1oabexg  5387  f1o00  5410  f1o0  5412  fnbrfvb  5470  fnrnfv  5476  funfvdm  5492  fvmptg  5505  fvmptd  5510  fvmpt2d  5515  fvmptdf  5516  mpteqb  5519  fvmptt  5520  funfvop  5540  eldmrexrn  5569  fvmptelrn  5581  fmpttd  5583  fmpt2d  5590  fmptco  5594  fmptcof  5595  fnasrn  5606  fnasrng  5608  mptexg  5653  eufnfv  5656  idref  5666  f1elima  5682  fliftrel  5701  fliftel  5702  fliftel1  5703  fliftcnv  5704  fliftf  5708  riotabiia  5755  acexmidlem2  5779  acexmidlemv  5780  oprabbii  5834  mpoeq12  5839  ovmpodxf  5904  ovmpodf  5910  ov6g  5916  f1ocnvd  5980  f1opw2  5984  suppssfv  5986  suppssov1  5987  ofvalg  5999  off  6002  offval2  6005  ofrfval2  6006  caofinvl  6012  abrexex  6023  abrexexg  6024  offres  6041  ofmres  6042  op1steq  6085  reldm  6092  mpoexga  6118  mpoex  6119  fnmpoovd  6120  fmpoco  6121  cnvf1o  6130  f1od2  6140  tposssxp  6154  brtpos2  6156  tpos0  6179  iunon  6189  tfrfun  6225  tfr2a  6226  tfrlemisucfn  6229  tfri1d  6240  tfr1onlemsucfn  6245  tfr1onlemubacc  6251  tfr1on  6255  tfri1dALT  6256  tfrcllemubacc  6264  tfrex  6273  rdgfun  6278  rdgon  6291  rdg0  6292  frec0g  6302  frecfnom  6306  freccllem  6307  freccl  6308  frecfcllem  6309  frecfcl  6310  frecsuclem  6311  0lt1o  6345  oafnex  6348  omfnex  6353  fnoei  6356  oeiexg  6357  oeiv  6360  oacl  6364  omcl  6365  oeicl  6366  oav2  6367  omv2  6369  eqer  6469  ecelqsg  6490  elqsn0m  6505  qsel  6514  qliftf  6522  ecoptocl  6524  eroprf  6530  ecopovsym  6533  ecopovtrn  6534  ecopovsymg  6536  ecopovtrng  6537  th3qlem2  6540  th3q  6542  mapsncnv  6597  mapsnf1o3  6599  mptelixpg  6636  ixpsnf1o  6638  en2d  6670  en3d  6671  dom2lem  6674  dom2  6677  1domsn  6721  xpcomen  6729  xpf1o  6746  mapxpen  6750  fidifsnen  6772  isbth  6863  elfir  6869  supsnti  6900  djueq1  6933  djueq2  6934  djuf1olem  6946  inl11  6958  updjud  6975  omp1eom  6988  difinfsn  6993  ctmlemr  7001  ctssdclemn0  7003  ctssdclemr  7005  ctssdc  7006  enumct  7008  nnnninf  7031  ismkvnex  7037  mkvprop  7040  exmidonfin  7067  exmidaclem  7081  exmidac  7082  cc3  7100  0npi  7145  indpi  7174  recidnq  7225  addnnnq0  7281  mulnnnq0  7282  genpprecll  7346  genppreclu  7347  caucvgprpr  7544  addsrpr  7577  mulsrpr  7578  0nsr  7581  00sr  7601  caucvgsrlemgt1  7627  opelreal  7659  eqresr  7668  axprecex  7712  nntopi  7726  axpre-suploc  7734  ltxrlt  7854  pncan3  7994  apreim  8389  divcanap2  8464  divcanap3  8482  lble  8729  sup3exmid  8739  nn1gt1  8778  0nn0  9016  pnf0xnn0  9071  0z  9089  decaddm10  9264  decmulnc  9272  10p10e20  9300  4t4e16  9304  5t4e20  9307  6t3e18  9310  6t4e24  9311  6t5e30  9312  7t3e21  9315  7t4e28  9316  7t5e35  9317  7t6e42  9318  7t7e49  9319  8t3e24  9321  8t4e32  9322  8t5e40  9323  8t7e56  9325  8t8e64  9326  9t3e27  9328  9t4e36  9329  9t5e45  9330  9t6e54  9331  9t7e63  9332  9t8e72  9333  9t9e81  9334  infrenegsupex  9416  znq  9443  ltpnf  9597  mnflt  9599  mnfltpnf  9601  xnegpnf  9641  xnegmnf  9642  xaddpnf1  9659  xaddpnf2  9660  xaddmnf1  9661  xaddmnf2  9662  pnfaddmnf  9663  mnfaddpnf  9664  lincmb01cmp  9816  iccf1o  9817  iccen  9819  elfzuz2  9840  fseq1m1p1  9906  fz0tp  9932  flqdiv  10125  frec2uzzd  10204  frec2uzsucd  10205  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgsuctlem  10227  uzenom  10229  fzfig  10234  nnenom  10238  seqeq1  10252  seq3val  10262  seqvalcd  10263  seqf  10265  seq3p1  10266  seqovcd  10267  seqp1cd  10270  seq3feq2  10274  seq3feq  10276  monoord2  10281  ser3mono  10282  seq3split  10283  seq3caopr2  10286  iseqf1olemqk  10298  seq3f1olemqsumkj  10302  seq3f1olemstep  10305  seq3f1oleml  10307  seq3f1o  10308  seq3homo  10314  seq3z  10315  seqfeq3  10316  seq3distr  10317  ser0f  10319  ser3ge0  10321  ser3le  10322  exp0  10328  0exp  10359  sq0  10414  sq10  10490  sq10e99m1  10491  facnn  10505  fac0  10506  bcval5  10541  hashinfom  10556  hashennn  10558  hashcl  10559  hashfz1  10561  hashen  10562  hash0  10575  fihashdom  10581  hashun  10583  seq3coll  10617  shftfibg  10624  shftfib  10627  shftfn  10628  2shfti  10635  seq3shft  10642  cvg1n  10790  resqrexlemsqa  10828  negfi  11031  xrmaxiflemcom  11050  xrmaxif  11052  infxrnegsupex  11064  climconst2  11092  climres  11104  climshft  11105  serclim0  11106  climle  11135  clim2ser  11138  clim2ser2  11139  climub  11145  climcvg1n  11151  climcaucn  11152  serf0  11153  sumfct  11175  fsum3cvg  11179  summodclem2  11183  zsumdc  11185  fsum3  11188  isumz  11190  fsumf1o  11191  isumss  11192  fsum3cvg2  11195  fsumsersdc  11196  fsum3ser  11198  fsumcl2lem  11199  fsumadd  11207  fsumsplitf  11209  sumsnf  11210  isummulc2  11227  isumadd  11232  fsumcnv  11238  mptfzshft  11243  fsumrev  11244  fsumshft  11245  fsummulc2  11249  iserabs  11276  isumshft  11291  isum1p  11293  isumlessdc  11297  divcnv  11298  trireciplem  11301  trirecip  11302  expcnvap0  11303  expcnvre  11304  expcnv  11305  explecnv  11306  geolim  11312  geolim2  11313  geo2lim  11317  geoisum  11318  geoisumr  11319  geoisum1  11320  geoisum1c  11321  cvgratnnlemseq  11327  cvgratz  11333  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  clim2prod  11340  clim2divap  11341  prodfap0  11346  prodfrecap  11347  prodfdivap  11348  prodeq2w  11357  fproddccvg  11373  prodmodclem2  11378  zproddc  11380  fprodseq  11384  efcllemp  11401  efval  11404  eff  11406  efcvgfsum  11410  reefcl  11411  ege2le3  11414  ef0  11415  efcj  11416  efaddlem  11417  efadd  11418  eftlcl  11431  reeftlcl  11432  eftlub  11433  efsep  11434  effsumlt  11435  efgt1p2  11438  efgt1p  11439  eflegeo  11444  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  eirraplem  11519  eirrap  11520  egt2lt3  11522  dvdsmul2  11552  odd2np1lem  11605  gcd0val  11685  gcd0id  11703  bezoutlemnewy  11720  eucalgcvga  11775  eucalg  11776  lcm0val  11782  qnumdencoprm  11907  qeqnumdivden  11908  phimul  11938  hashgcdeq  11940  xpnnen  11943  ennnfonelemk  11949  ennnfonelemj0  11950  ennnfonelem0  11954  ennnfonelemnn0  11971  ctinfom  11977  ctiunct  11989  ressid  12059  2strstr1g  12101  srngstrd  12120  ipsstrd  12139  elrest  12166  elrestr  12167  topnpropgd  12173  toptopon2  12225  toponmax  12231  tpstop  12241  tpspropd  12242  tsettps  12244  eltpsg  12246  tgiun  12281  ntrval  12318  clsval  12319  0cld  12320  uncld  12321  cldcls  12322  ntr0  12342  isopn3i  12343  neif  12349  neival  12351  neii2  12357  neiss  12358  opnneiss  12366  innei  12371  neissex  12373  tgrest  12377  stoig  12381  restco  12382  resttopon2  12386  restopn2  12391  cnpval  12406  cntop1  12409  cntop2  12410  cnprcl2k  12414  lmcvg  12425  iscnp4  12426  cnima  12428  cnco  12429  cnclima  12431  cnntri  12432  cnntr  12433  cnss1  12434  cnss2  12435  cncnpi  12436  cncnp  12438  cnrest  12443  cnrest2  12444  cnrest2r  12445  lmss  12454  lmres  12456  lmcn  12459  txuni2  12464  txbasex  12465  eltx  12467  txtop  12468  txtopon  12470  txopn  12473  txss12  12474  txbasval  12475  neitx  12476  txcnp  12479  upxp  12480  txcnmpt  12481  uptx  12482  txcn  12483  txrest  12484  txdis1cn  12486  txlm  12487  lmcn2  12488  cnmpt11  12491  cnmpt11f  12492  cnmpt1t  12493  cnmpt12  12495  cnmpt21  12499  cnmpt21f  12500  cnmpt2t  12501  cnmpt22  12502  cnmpt1res  12504  cnmpt2res  12505  cnmptcom  12506  imasnopn  12507  hmeocnv  12515  hmeoopn  12519  hmeocld  12520  hmeontr  12521  hmeoimaf1o  12522  hmeores  12523  txhmeo  12527  txswaphmeo  12529  xmet0  12571  blfvalps  12593  blfps  12617  blf  12618  blpnfctr  12647  xmetresbl  12648  isxms2  12660  xmstps  12665  msxms  12666  xmsxmet  12668  msmet  12669  xmspropd  12685  mspropd  12686  neibl  12699  bdxmet  12709  bdmopn  12712  mopnex  12713  xmetxp  12715  xmettxlem  12717  xmettx  12718  txmetcnp  12726  metcnpd  12728  cnmet  12738  unicntopcntop  12744  cnopncntop  12745  remetdval  12747  resubmet  12756  tgioo2cntop  12757  addcncntoplem  12759  divcnap  12763  fsumcncntop  12764  divccncfap  12785  cncfmet  12787  cncfcncntop  12788  cncfmptc  12790  cncfmptid  12791  cncfmpt1f  12792  cncfmpt2fcntop  12793  cdivcncfap  12795  negfcncf  12797  mulcncflem  12798  mulcncf  12799  cnopnap  12802  ivthinc  12829  ivthdec  12830  limcmpted  12840  limcimolemlt  12841  cnplimcim  12844  cnplimclemr  12846  cnlimcim  12848  cnlimc  12849  cnmptlimc  12851  limccnpcntop  12852  limccnp2lem  12853  limccnp2cntop  12854  reldvg  12856  dvfvalap  12858  dvcl  12860  dvbss  12862  dvfgg  12865  dvidlemap  12868  dvcnp2cntop  12871  dvcn  12872  dvaddxxbr  12873  dvmulxxbr  12874  dvaddxx  12875  dvmulxx  12876  dviaddf  12877  dvimulf  12878  dvcoapbr  12879  dvcjbr  12880  dvrecap  12885  dveflem  12895  dvef  12896  sincn  12898  coscn  12899  ex-or  13105  ex-an  13106  1kp2ke3k  13107  ex-exp  13110  ex-fac  13111  bj-2inf  13307  bj-inf2vnlem1  13339  subctctexmid  13369  nnsf  13374  peano3nninf  13376  nninfalllemn  13377  nninfself  13384  nninfsellemeqinf  13387  nninffeq  13391  trilpolemcl  13405  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  dceqnconst  13423  iooreen  13427