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  10007  iseqval  10017  iseqvalt  10019  seq3val  10020  iseq1  10021  iseqfcl  10024  iseqfclt  10025  seqf  10026  iseqcl  10027  iseqp1  10028  iseqp1t  10029  seq3p1  10030  iseqsst  10031  seq3feq2  10035  seq3feq  10037  monoord2  10043  ser3mono  10044  seq3split  10045  seq3caopr2  10048  iseqf1olemqk  10060  seq3f1olemqsumkj  10064  seq3f1olemstep  10067  seq3f1oleml  10069  seq3f1o  10070  seq3homo  10076  seq3z  10077  seqfeq3  10078  seq3distr  10079  ser0f  10081  ser3ge0  10083  ser3le  10084  exp0  10090  0exp  10121  sq0  10176  sq10  10252  sq10e99m1  10253  facnn  10266  fac0  10267  bcval5  10302  hashinfom  10317  hashennn  10319  hashcl  10320  hashfz1  10322  hashen  10323  hash0  10336  fihashdom  10342  hashun  10344  seq3coll  10378  shftfibg  10385  shftfib  10388  shftfn  10389  2shfti  10396  seq3shft  10403  cvg1n  10550  resqrexlemsqa  10588  negfi  10790  xrmaxiflemcom  10808  xrmaxif  10810  infxrnegsupex  10822  climconst2  10850  climres  10862  climshft  10863  serclim0  10864  climle  10893  clim2ser  10896  clim2ser2  10897  climub  10903  climcvg1n  10909  climcaucn  10910  serf0  10911  sumfct  10933  fsum3cvg  10936  summodclem2  10941  zsumdc  10943  fsum3  10946  isumz  10948  fsumf1o  10949  isumss  10950  fsum3cvg2  10953  fsumsersdc  10954  fsum3ser  10956  fsumcl2lem  10957  fsumadd  10965  fsumsplitf  10967  sumsnf  10968  isummulc2  10985  isumadd  10990  fsumcnv  10996  mptfzshft  11001  fsumrev  11002  fsumshft  11003  fsummulc2  11007  iserabs  11034  isumshft  11049  isum1p  11051  isumlessdc  11055  divcnv  11056  trireciplem  11059  trirecip  11060  expcnvap0  11061  expcnvre  11062  expcnv  11063  explecnv  11064  geolim  11070  geolim2  11071  geo2lim  11075  geoisum  11076  geoisumr  11077  geoisum1  11078  geoisum1c  11079  cvgratnnlemseq  11085  cvgratz  11091  mertenslemub  11093  mertenslemi1  11094  mertenslem2  11095  mertensabs  11096  efcllemp  11113  efval  11116  eff  11118  efcvgfsum  11122  reefcl  11123  ege2le3  11126  ef0  11127  efcj  11128  efaddlem  11129  efadd  11130  eftlcl  11143  reeftlcl  11144  eftlub  11145  efsep  11146  effsumlt  11147  efgt1p2  11150  efgt1p  11151  eflegeo  11157  ef01bndlem  11212  sin01bnd  11213  cos01bnd  11214  eirraplem  11229  eirrap  11230  egt2lt3  11232  dvdsmul2  11262  odd2np1lem  11315  gcd0val  11395  gcd0id  11413  bezoutlemnewy  11428  eucalgcvga  11483  eucalg  11484  lcm0val  11490  qnumdencoprm  11614  qeqnumdivden  11615  phimul  11645  hashgcdeq  11647  xpnnen  11650  ressid  11720  2strstr1g  11762  srngstrd  11781  ipsstrd  11800  elrest  11827  elrestr  11828  topnpropgd  11834  toptopon2  11886  toponmax  11891  tpstop  11901  tpspropd  11902  tsettps  11904  eltpsg  11906  tgiun  11941  ntrval  11978  clsval  11979  0cld  11980  uncld  11981  cldcls  11982  ntr0  12002  isopn3i  12003  neif  12009  neival  12011  neii2  12017  neiss  12018  opnneiss  12026  innei  12031  neissex  12033  tgrest  12037  stoig  12041  restco  12042  resttopon2  12046  restopn2  12051  cnpval  12065  cntop1  12068  cntop2  12069  cnprcl2k  12073  lmcvg  12084  iscnp4  12085  cnima  12087  cnco  12088  cnclima  12090  cnntri  12091  cnntr  12092  cnss1  12093  cnss2  12094  cncnpi  12095  cncnp  12097  cnrest  12102  cnrest2  12103  cnrest2r  12104  lmss  12113  lmres  12115  lmcn  12118  cnmpt11  12121  cnmpt11f  12122  cnmpt1res  12123  xmet0  12165  blfvalps  12187  blfps  12211  blf  12212  blpnfctr  12241  xmetresbl  12242  isxms2  12254  xmstps  12259  msxms  12260  xmsxmet  12262  msmet  12263  xmspropd  12279  mspropd  12280  neibl  12293  bdxmet  12303  bdmopn  12306  mopnex  12307  cnmet  12325  remetdval  12329  resubmet  12338  divccncfap  12359  cncfmet  12361  cncfmptc  12362  cncfmptid  12363  cncfmpt1f  12364  cdivcncfap  12366  negfcncf  12368  mulcncflem  12369  mulcncf  12370  ex-or  12373  ex-an  12374  1kp2ke3k  12375  ex-exp  12378  ex-fac  12379  bj-2inf  12557  bj-inf2vnlem1  12589  nnsf  12616  peano3nninf  12618  nninfalllemn  12619  nninfself  12626  nninfsellemeqinf  12629