Theorem eqid 2095

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

Syntax hints:   = wceq 1296   e. wcel 1445

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

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

This theorem is referenced by:  eqidd  2096  neirr  2271  sbsbc  2858  sbceqal  2908  dfnul2  3304  snidg  3493  prid1g  3566  tpid1  3573  tpid1g  3574  tpid2  3575  tpid2g  3576  tpid3  3578  dfiin2g  3785  syl5eqbr  3900  syl5eqbrr  3901  syl6breq  3906  opabbii  3927  mpteq2ia  3946  mpteq2da  3949  sucidg  4267  onsucelsucexmidlem1  4372  regexmidlemm  4376  regexmidlem1  4377  reg2exmidlema  4378  regexmid  4379  reg2exmid  4380  reg3exmid  4423  tfisi  4430  finds1  4445  nn0suc  4447  nndceq0  4459  0elnn  4460  nnregexmid  4462  opelxp  4497  relopab  4594  relop  4617  ididg  4620  elrnmpt1s  4717  dfiun3g  4722  dfiin3g  4723  dmmptg  4962  funfn  5079  mpt0  5175  f0  5236  dffn4  5274  f1orn  5298  f1oabexg  5300  f1o00  5323  f1o0  5325  fnbrfvb  5380  fnrnfv  5386  funfvdm  5402  fvmptg  5415  fvmptd  5420  fvmpt2d  5425  fvmptdf  5426  mpteqb  5429  fvmptt  5430  funfvop  5450  eldmrexrn  5479  fmpttd  5492  fmpt2d  5499  fmptco  5503  fmptcof  5504  fnasrn  5514  fnasrng  5516  mptexg  5561  eufnfv  5564  idref  5574  f1elima  5590  fliftrel  5609  fliftel  5610  fliftel1  5611  fliftcnv  5612  fliftf  5616  riotabiia  5663  acexmidlem2  5687  acexmidlemv  5688  oprabbii  5742  mpt2eq12  5747  ovmpt2dxf  5808  ovmpt2df  5814  ov6g  5820  f1ocnvd  5884  f1opw2  5888  suppssfv  5890  suppssov1  5891  fnofval  5903  off  5906  offval2  5908  ofrfval2  5909  caofinvl  5915  abrexex  5926  abrexexg  5927  offres  5944  ofmres  5945  op1steq  5987  reldm  5994  mpt2exga  6017  mpt2ex  6018  fmpt2co  6019  cnvf1o  6028  f1od2  6038  tposssxp  6052  brtpos2  6054  tpos0  6077  iunon  6087  tfrfun  6123  tfr2a  6124  tfrlemisucfn  6127  tfri1d  6138  tfr1onlemsucfn  6143  tfr1onlemubacc  6149  tfr1on  6153  tfri1dALT  6154  tfrcllemubacc  6162  tfrex  6171  rdgfun  6176  rdgon  6189  rdg0  6190  frec0g  6200  frecfnom  6204  freccllem  6205  freccl  6206  frecfcllem  6207  frecfcl  6208  frecsuclem  6209  0lt1o  6242  oafnex  6245  omfnex  6250  fnoei  6253  oeiexg  6254  oeiv  6257  oacl  6261  omcl  6262  oeicl  6263  oav2  6264  omv2  6266  eqer  6364  ecelqsg  6385  elqsn0m  6400  qsel  6409  qliftf  6417  ecoptocl  6419  eroprf  6425  ecopovsym  6428  ecopovtrn  6429  ecopovsymg  6431  ecopovtrng  6432  th3qlem2  6435  th3q  6437  mapsncnv  6492  mapsnf1o3  6494  mptelixpg  6531  ixpsnf1o  6533  en2d  6565  en3d  6566  dom2lem  6569  dom2  6572  1domsn  6615  xpcomen  6623  xpf1o  6640  mapxpen  6644  fidifsnen  6666  isbth  6756  supsnti  6780  djueq1  6813  djueq2  6814  djuf1olem  6825  updjud  6853  ctmlemr  6870  enumct  6873  nnnninf  6894  mkvprop  6901  0npi  6969  indpi  6998  recidnq  7049  addnnnq0  7105  mulnnnq0  7106  genpprecll  7170  genppreclu  7171  caucvgprpr  7368  addsrpr  7388  mulsrpr  7389  0nsr  7392  00sr  7412  caucvgsrlemgt1  7437  opelreal  7462  eqresr  7470  axprecex  7512  nntopi  7526  ltxrlt  7649  pncan3  7787  apreim  8177  divcanap2  8244  divcanap3  8262  lble  8505  sup3exmid  8515  nn1gt1  8554  0nn0  8786  pnf0xnn0  8841  0z  8859  decaddm10  9034  decmulnc  9042  10p10e20  9070  4t4e16  9074  5t4e20  9077  6t3e18  9080  6t4e24  9081  6t5e30  9082  7t3e21  9085  7t4e28  9086  7t5e35  9087  7t6e42  9088  7t7e49  9089  8t3e24  9091  8t4e32  9092  8t5e40  9093  8t7e56  9095  8t8e64  9096  9t3e27  9098  9t4e36  9099  9t5e45  9100  9t6e54  9101  9t7e63  9102  9t8e72  9103  9t9e81  9104  infrenegsupex  9181  znq  9208  ltpnf  9350  mnflt  9352  mnfltpnf  9354  xnegpnf  9394  xnegmnf  9395  xaddpnf1  9412  xaddpnf2  9413  xaddmnf1  9414  xaddmnf2  9415  pnfaddmnf  9416  mnfaddpnf  9417  lincmb01cmp  9569  iccf1o  9570  elfzuz2  9592  fseq1m1p1  9658  fz0tp  9684  flqdiv  9877  frec2uzzd  9956  frec2uzsucd  9957  frecuzrdgrrn  9964  frec2uzrdg  9965  frecuzrdgrcl  9966  frecuzrdgsuc  9970  frecuzrdgrclt  9971  frecuzrdgg  9972  frecuzrdgsuctlem  9979  uzenom  9981  fzfig  9986  nnenom  9990  seqeq1  10003  seq3val  10013  seqf  10015  seq3p1  10016  seq3feq2  10020  seq3feq  10022  monoord2  10027  ser3mono  10028  seq3split  10029  seq3caopr2  10032  iseqf1olemqk  10044  seq3f1olemqsumkj  10048  seq3f1olemstep  10051  seq3f1oleml  10053  seq3f1o  10054  seq3homo  10060  seq3z  10061  seqfeq3  10062  seq3distr  10063  ser0f  10065  ser3ge0  10067  ser3le  10068  exp0  10074  0exp  10105  sq0  10160  sq10  10236  sq10e99m1  10237  facnn  10250  fac0  10251  bcval5  10286  hashinfom  10301  hashennn  10303  hashcl  10304  hashfz1  10306  hashen  10307  hash0  10320  fihashdom  10326  hashun  10328  seq3coll  10362  shftfibg  10369  shftfib  10372  shftfn  10373  2shfti  10380  seq3shft  10387  cvg1n  10534  resqrexlemsqa  10572  negfi  10774  xrmaxiflemcom  10792  xrmaxif  10794  infxrnegsupex  10806  climconst2  10834  climres  10846  climshft  10847  serclim0  10848  climle  10877  clim2ser  10880  clim2ser2  10881  climub  10887  climcvg1n  10893  climcaucn  10894  serf0  10895  sumfct  10917  fsum3cvg  10920  summodclem2  10925  zsumdc  10927  fsum3  10930  isumz  10932  fsumf1o  10933  isumss  10934  fsum3cvg2  10937  fsumsersdc  10938  fsum3ser  10940  fsumcl2lem  10941  fsumadd  10949  fsumsplitf  10951  sumsnf  10952  isummulc2  10969  isumadd  10974  fsumcnv  10980  mptfzshft  10985  fsumrev  10986  fsumshft  10987  fsummulc2  10991  iserabs  11018  isumshft  11033  isum1p  11035  isumlessdc  11039  divcnv  11040  trireciplem  11043  trirecip  11044  expcnvap0  11045  expcnvre  11046  expcnv  11047  explecnv  11048  geolim  11054  geolim2  11055  geo2lim  11059  geoisum  11060  geoisumr  11061  geoisum1  11062  geoisum1c  11063  cvgratnnlemseq  11069  cvgratz  11075  mertenslemub  11077  mertenslemi1  11078  mertenslem2  11079  mertensabs  11080  efcllemp  11097  efval  11100  eff  11102  efcvgfsum  11106  reefcl  11107  ege2le3  11110  ef0  11111  efcj  11112  efaddlem  11113  efadd  11114  eftlcl  11127  reeftlcl  11128  eftlub  11129  efsep  11130  effsumlt  11131  efgt1p2  11134  efgt1p  11135  eflegeo  11141  ef01bndlem  11196  sin01bnd  11197  cos01bnd  11198  eirraplem  11213  eirrap  11214  egt2lt3  11216  dvdsmul2  11246  odd2np1lem  11299  gcd0val  11379  gcd0id  11397  bezoutlemnewy  11412  eucalgcvga  11467  eucalg  11468  lcm0val  11474  qnumdencoprm  11598  qeqnumdivden  11599  phimul  11629  hashgcdeq  11631  xpnnen  11634  ressid  11704  2strstr1g  11746  srngstrd  11765  ipsstrd  11784  elrest  11811  elrestr  11812  topnpropgd  11818  toptopon2  11870  toponmax  11875  tpstop  11885  tpspropd  11886  tsettps  11888  eltpsg  11890  tgiun  11925  ntrval  11962  clsval  11963  0cld  11964  uncld  11965  cldcls  11966  ntr0  11986  isopn3i  11987  neif  11993  neival  11995  neii2  12001  neiss  12002  opnneiss  12010  innei  12015  neissex  12017  tgrest  12021  stoig  12025  restco  12026  resttopon2  12030  restopn2  12035  cnpval  12049  cntop1  12052  cntop2  12053  cnprcl2k  12057  lmcvg  12068  iscnp4  12069  cnima  12071  cnco  12072  cnclima  12074  cnntri  12075  cnntr  12076  cnss1  12077  cnss2  12078  cncnpi  12079  cncnp  12081  cnrest  12086  cnrest2  12087  cnrest2r  12088  lmss  12097  lmres  12099  lmcn  12102  cnmpt11  12105  cnmpt11f  12106  cnmpt1res  12107  xmet0  12149  blfvalps  12171  blfps  12195  blf  12196  blpnfctr  12225  xmetresbl  12226  isxms2  12238  xmstps  12243  msxms  12244  xmsxmet  12246  msmet  12247  xmspropd  12263  mspropd  12264  neibl  12277  bdxmet  12287  bdmopn  12290  mopnex  12291  cnmet  12309  remetdval  12313  resubmet  12322  divccncfap  12343  cncfmet  12345  cncfmptc  12346  cncfmptid  12347  cncfmpt1f  12348  cdivcncfap  12350  negfcncf  12352  mulcncflem  12353  mulcncf  12354  ex-or  12357  ex-an  12358  1kp2ke3k  12359  ex-exp  12362  ex-fac  12363  bj-2inf  12541  bj-inf2vnlem1  12573  nnsf  12600  peano3nninf  12602  nninfalllemn  12603  nninfself  12610  nninfsellemeqinf  12613