Theorem eqid 2137

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

Syntax hints:   = wceq 1331   e. wcel 1480

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 1425  ax-ext 2119

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

This theorem is referenced by:  eqidd  2138  neirr  2315  sbsbc  2908  sbceqal  2959  dfnul2  3360  snidg  3549  prid1g  3622  tpid1  3629  tpid1g  3630  tpid2  3631  tpid2g  3632  tpid3  3634  dfiin2g  3841  eqbrtrid  3958  eqbrtrrid  3959  breqtrdi  3964  opabbii  3990  mpteq2ia  4009  mpteq2da  4012  sucidg  4333  onsucelsucexmidlem1  4438  regexmidlemm  4442  regexmidlem1  4443  reg2exmidlema  4444  regexmid  4445  reg2exmid  4446  reg3exmid  4489  tfisi  4496  finds1  4511  nn0suc  4513  nndceq0  4526  0elnn  4527  nnregexmid  4529  opelxp  4564  relopab  4661  relop  4684  ididg  4687  elrnmpt1s  4784  dfiun3g  4791  dfiin3g  4792  dmmptg  5031  funfn  5148  mpt0  5245  f0  5308  dffn4  5346  f1orn  5370  f1oabexg  5372  f1o00  5395  f1o0  5397  fnbrfvb  5455  fnrnfv  5461  funfvdm  5477  fvmptg  5490  fvmptd  5495  fvmpt2d  5500  fvmptdf  5501  mpteqb  5504  fvmptt  5505  funfvop  5525  eldmrexrn  5554  fvmptelrn  5566  fmpttd  5568  fmpt2d  5575  fmptco  5579  fmptcof  5580  fnasrn  5591  fnasrng  5593  mptexg  5638  eufnfv  5641  idref  5651  f1elima  5667  fliftrel  5686  fliftel  5687  fliftel1  5688  fliftcnv  5689  fliftf  5693  riotabiia  5740  acexmidlem2  5764  acexmidlemv  5765  oprabbii  5819  mpoeq12  5824  ovmpodxf  5889  ovmpodf  5895  ov6g  5901  f1ocnvd  5965  f1opw2  5969  suppssfv  5971  suppssov1  5972  ofvalg  5984  off  5987  offval2  5990  ofrfval2  5991  caofinvl  5997  abrexex  6008  abrexexg  6009  offres  6026  ofmres  6027  op1steq  6070  reldm  6077  mpoexga  6103  mpoex  6104  fnmpoovd  6105  fmpoco  6106  cnvf1o  6115  f1od2  6125  tposssxp  6139  brtpos2  6141  tpos0  6164  iunon  6174  tfrfun  6210  tfr2a  6211  tfrlemisucfn  6214  tfri1d  6225  tfr1onlemsucfn  6230  tfr1onlemubacc  6236  tfr1on  6240  tfri1dALT  6241  tfrcllemubacc  6249  tfrex  6258  rdgfun  6263  rdgon  6276  rdg0  6277  frec0g  6287  frecfnom  6291  freccllem  6292  freccl  6293  frecfcllem  6294  frecfcl  6295  frecsuclem  6296  0lt1o  6330  oafnex  6333  omfnex  6338  fnoei  6341  oeiexg  6342  oeiv  6345  oacl  6349  omcl  6350  oeicl  6351  oav2  6352  omv2  6354  eqer  6454  ecelqsg  6475  elqsn0m  6490  qsel  6499  qliftf  6507  ecoptocl  6509  eroprf  6515  ecopovsym  6518  ecopovtrn  6519  ecopovsymg  6521  ecopovtrng  6522  th3qlem2  6525  th3q  6527  mapsncnv  6582  mapsnf1o3  6584  mptelixpg  6621  ixpsnf1o  6623  en2d  6655  en3d  6656  dom2lem  6659  dom2  6662  1domsn  6706  xpcomen  6714  xpf1o  6731  mapxpen  6735  fidifsnen  6757  isbth  6848  elfir  6854  supsnti  6885  djueq1  6918  djueq2  6919  djuf1olem  6931  inl11  6943  updjud  6960  omp1eom  6973  difinfsn  6978  ctmlemr  6986  ctssdclemn0  6988  ctssdclemr  6990  ctssdc  6991  enumct  6993  nnnninf  7016  ismkvnex  7022  mkvprop  7025  exmidonfin  7043  exmidaclem  7057  exmidac  7058  0npi  7114  indpi  7143  recidnq  7194  addnnnq0  7250  mulnnnq0  7251  genpprecll  7315  genppreclu  7316  caucvgprpr  7513  addsrpr  7546  mulsrpr  7547  0nsr  7550  00sr  7570  caucvgsrlemgt1  7596  opelreal  7628  eqresr  7637  axprecex  7681  nntopi  7695  axpre-suploc  7703  ltxrlt  7823  pncan3  7963  apreim  8358  divcanap2  8433  divcanap3  8451  lble  8698  sup3exmid  8708  nn1gt1  8747  0nn0  8985  pnf0xnn0  9040  0z  9058  decaddm10  9233  decmulnc  9241  10p10e20  9269  4t4e16  9273  5t4e20  9276  6t3e18  9279  6t4e24  9280  6t5e30  9281  7t3e21  9284  7t4e28  9285  7t5e35  9286  7t6e42  9287  7t7e49  9288  8t3e24  9290  8t4e32  9291  8t5e40  9292  8t7e56  9294  8t8e64  9295  9t3e27  9297  9t4e36  9298  9t5e45  9299  9t6e54  9300  9t7e63  9301  9t8e72  9302  9t9e81  9303  infrenegsupex  9382  znq  9409  ltpnf  9560  mnflt  9562  mnfltpnf  9564  xnegpnf  9604  xnegmnf  9605  xaddpnf1  9622  xaddpnf2  9623  xaddmnf1  9624  xaddmnf2  9625  pnfaddmnf  9626  mnfaddpnf  9627  lincmb01cmp  9779  iccf1o  9780  elfzuz2  9802  fseq1m1p1  9868  fz0tp  9894  flqdiv  10087  frec2uzzd  10166  frec2uzsucd  10167  frecuzrdgrrn  10174  frec2uzrdg  10175  frecuzrdgrcl  10176  frecuzrdgsuc  10180  frecuzrdgrclt  10181  frecuzrdgg  10182  frecuzrdgsuctlem  10189  uzenom  10191  fzfig  10196  nnenom  10200  seqeq1  10214  seq3val  10224  seqvalcd  10225  seqf  10227  seq3p1  10228  seqovcd  10229  seqp1cd  10232  seq3feq2  10236  seq3feq  10238  monoord2  10243  ser3mono  10244  seq3split  10245  seq3caopr2  10248  iseqf1olemqk  10260  seq3f1olemqsumkj  10264  seq3f1olemstep  10267  seq3f1oleml  10269  seq3f1o  10270  seq3homo  10276  seq3z  10277  seqfeq3  10278  seq3distr  10279  ser0f  10281  ser3ge0  10283  ser3le  10284  exp0  10290  0exp  10321  sq0  10376  sq10  10452  sq10e99m1  10453  facnn  10466  fac0  10467  bcval5  10502  hashinfom  10517  hashennn  10519  hashcl  10520  hashfz1  10522  hashen  10523  hash0  10536  fihashdom  10542  hashun  10544  seq3coll  10578  shftfibg  10585  shftfib  10588  shftfn  10589  2shfti  10596  seq3shft  10603  cvg1n  10751  resqrexlemsqa  10789  negfi  10992  xrmaxiflemcom  11011  xrmaxif  11013  infxrnegsupex  11025  climconst2  11053  climres  11065  climshft  11066  serclim0  11067  climle  11096  clim2ser  11099  clim2ser2  11100  climub  11106  climcvg1n  11112  climcaucn  11113  serf0  11114  sumfct  11136  fsum3cvg  11139  summodclem2  11144  zsumdc  11146  fsum3  11149  isumz  11151  fsumf1o  11152  isumss  11153  fsum3cvg2  11156  fsumsersdc  11157  fsum3ser  11159  fsumcl2lem  11160  fsumadd  11168  fsumsplitf  11170  sumsnf  11171  isummulc2  11188  isumadd  11193  fsumcnv  11199  mptfzshft  11204  fsumrev  11205  fsumshft  11206  fsummulc2  11210  iserabs  11237  isumshft  11252  isum1p  11254  isumlessdc  11258  divcnv  11259  trireciplem  11262  trirecip  11263  expcnvap0  11264  expcnvre  11265  expcnv  11266  explecnv  11267  geolim  11273  geolim2  11274  geo2lim  11278  geoisum  11279  geoisumr  11280  geoisum1  11281  geoisum1c  11282  cvgratnnlemseq  11288  cvgratz  11294  mertenslemub  11296  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  clim2prod  11301  clim2divap  11302  prodfap0  11307  prodfrecap  11308  prodfdivap  11309  prodeq2w  11318  fproddccvg  11334  efcllemp  11353  efval  11356  eff  11358  efcvgfsum  11362  reefcl  11363  ege2le3  11366  ef0  11367  efcj  11368  efaddlem  11369  efadd  11370  eftlcl  11383  reeftlcl  11384  eftlub  11385  efsep  11386  effsumlt  11387  efgt1p2  11390  efgt1p  11391  eflegeo  11397  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  eirraplem  11472  eirrap  11473  egt2lt3  11475  dvdsmul2  11505  odd2np1lem  11558  gcd0val  11638  gcd0id  11656  bezoutlemnewy  11673  eucalgcvga  11728  eucalg  11729  lcm0val  11735  qnumdencoprm  11860  qeqnumdivden  11861  phimul  11891  hashgcdeq  11893  xpnnen  11896  ennnfonelemk  11902  ennnfonelemj0  11903  ennnfonelem0  11907  ennnfonelemnn0  11924  ctinfom  11930  ctiunct  11942  ressid  12009  2strstr1g  12051  srngstrd  12070  ipsstrd  12089  elrest  12116  elrestr  12117  topnpropgd  12123  toptopon2  12175  toponmax  12181  tpstop  12191  tpspropd  12192  tsettps  12194  eltpsg  12196  tgiun  12231  ntrval  12268  clsval  12269  0cld  12270  uncld  12271  cldcls  12272  ntr0  12292  isopn3i  12293  neif  12299  neival  12301  neii2  12307  neiss  12308  opnneiss  12316  innei  12321  neissex  12323  tgrest  12327  stoig  12331  restco  12332  resttopon2  12336  restopn2  12341  cnpval  12356  cntop1  12359  cntop2  12360  cnprcl2k  12364  lmcvg  12375  iscnp4  12376  cnima  12378  cnco  12379  cnclima  12381  cnntri  12382  cnntr  12383  cnss1  12384  cnss2  12385  cncnpi  12386  cncnp  12388  cnrest  12393  cnrest2  12394  cnrest2r  12395  lmss  12404  lmres  12406  lmcn  12409  txuni2  12414  txbasex  12415  eltx  12417  txtop  12418  txtopon  12420  txopn  12423  txss12  12424  txbasval  12425  neitx  12426  txcnp  12429  upxp  12430  txcnmpt  12431  uptx  12432  txcn  12433  txrest  12434  txdis1cn  12436  txlm  12437  lmcn2  12438  cnmpt11  12441  cnmpt11f  12442  cnmpt1t  12443  cnmpt12  12445  cnmpt21  12449  cnmpt21f  12450  cnmpt2t  12451  cnmpt22  12452  cnmpt1res  12454  cnmpt2res  12455  cnmptcom  12456  imasnopn  12457  hmeocnv  12465  hmeoopn  12469  hmeocld  12470  hmeontr  12471  hmeoimaf1o  12472  hmeores  12473  txhmeo  12477  txswaphmeo  12479  xmet0  12521  blfvalps  12543  blfps  12567  blf  12568  blpnfctr  12597  xmetresbl  12598  isxms2  12610  xmstps  12615  msxms  12616  xmsxmet  12618  msmet  12619  xmspropd  12635  mspropd  12636  neibl  12649  bdxmet  12659  bdmopn  12662  mopnex  12663  xmetxp  12665  xmettxlem  12667  xmettx  12668  txmetcnp  12676  metcnpd  12678  cnmet  12688  unicntopcntop  12694  cnopncntop  12695  remetdval  12697  resubmet  12706  tgioo2cntop  12707  addcncntoplem  12709  divcnap  12713  fsumcncntop  12714  divccncfap  12735  cncfmet  12737  cncfcncntop  12738  cncfmptc  12740  cncfmptid  12741  cncfmpt1f  12742  cncfmpt2fcntop  12743  cdivcncfap  12745  negfcncf  12747  mulcncflem  12748  mulcncf  12749  cnopnap  12752  ivthinc  12779  ivthdec  12780  limcmpted  12790  limcimolemlt  12791  cnplimcim  12794  cnplimclemr  12796  cnlimcim  12798  cnlimc  12799  cnmptlimc  12801  limccnpcntop  12802  limccnp2lem  12803  limccnp2cntop  12804  reldvg  12806  dvfvalap  12808  dvcl  12810  dvbss  12812  dvfgg  12815  dvidlemap  12818  dvcnp2cntop  12821  dvcn  12822  dvaddxxbr  12823  dvmulxxbr  12824  dvaddxx  12825  dvmulxx  12826  dviaddf  12827  dvimulf  12828  dvcoapbr  12829  dvcjbr  12830  dvrecap  12835  dveflem  12844  dvef  12845  sincn  12847  coscn  12848  ex-or  12923  ex-an  12924  1kp2ke3k  12925  ex-exp  12928  ex-fac  12929  bj-2inf  13125  bj-inf2vnlem1  13157  subctctexmid  13185  nnsf  13188  peano3nninf  13190  nninfalllemn  13191  nninfself  13198  nninfsellemeqinf  13201  nninffeq  13205  trilpolemcl  13219  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223