Theorem eqid 2139

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	⊢ 𝐴 = 𝐴

Proof of Theorem eqid

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		biid 170	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
2	1	eqriv 2136	1 ⊢ 𝐴 = 𝐴

Syntax hints:   = wceq 1331   ∈ 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 2121

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

This theorem is referenced by:  eqidd  2140  neirr  2317  sbsbc  2913  sbceqal  2964  dfnul2  3365  snidg  3554  prid1g  3627  tpid1  3634  tpid1g  3635  tpid2  3636  tpid2g  3637  tpid3  3639  dfiin2g  3846  eqbrtrid  3963  eqbrtrrid  3964  breqtrdi  3969  opabbii  3995  mpteq2ia  4014  mpteq2da  4017  sucidg  4338  onsucelsucexmidlem1  4443  regexmidlemm  4447  regexmidlem1  4448  reg2exmidlema  4449  regexmid  4450  reg2exmid  4451  reg3exmid  4494  tfisi  4501  finds1  4516  nn0suc  4518  nndceq0  4531  0elnn  4532  nnregexmid  4534  opelxp  4569  relopab  4666  relop  4689  ididg  4692  elrnmpt1s  4789  dfiun3g  4796  dfiin3g  4797  dmmptg  5036  funfn  5153  mpt0  5250  f0  5313  dffn4  5351  f1orn  5377  f1oabexg  5379  f1o00  5402  f1o0  5404  fnbrfvb  5462  fnrnfv  5468  funfvdm  5484  fvmptg  5497  fvmptd  5502  fvmpt2d  5507  fvmptdf  5508  mpteqb  5511  fvmptt  5512  funfvop  5532  eldmrexrn  5561  fvmptelrn  5573  fmpttd  5575  fmpt2d  5582  fmptco  5586  fmptcof  5587  fnasrn  5598  fnasrng  5600  mptexg  5645  eufnfv  5648  idref  5658  f1elima  5674  fliftrel  5693  fliftel  5694  fliftel1  5695  fliftcnv  5696  fliftf  5700  riotabiia  5747  acexmidlem2  5771  acexmidlemv  5772  oprabbii  5826  mpoeq12  5831  ovmpodxf  5896  ovmpodf  5902  ov6g  5908  f1ocnvd  5972  f1opw2  5976  suppssfv  5978  suppssov1  5979  ofvalg  5991  off  5994  offval2  5997  ofrfval2  5998  caofinvl  6004  abrexex  6015  abrexexg  6016  offres  6033  ofmres  6034  op1steq  6077  reldm  6084  mpoexga  6110  mpoex  6111  fnmpoovd  6112  fmpoco  6113  cnvf1o  6122  f1od2  6132  tposssxp  6146  brtpos2  6148  tpos0  6171  iunon  6181  tfrfun  6217  tfr2a  6218  tfrlemisucfn  6221  tfri1d  6232  tfr1onlemsucfn  6237  tfr1onlemubacc  6243  tfr1on  6247  tfri1dALT  6248  tfrcllemubacc  6256  tfrex  6265  rdgfun  6270  rdgon  6283  rdg0  6284  frec0g  6294  frecfnom  6298  freccllem  6299  freccl  6300  frecfcllem  6301  frecfcl  6302  frecsuclem  6303  0lt1o  6337  oafnex  6340  omfnex  6345  fnoei  6348  oeiexg  6349  oeiv  6352  oacl  6356  omcl  6357  oeicl  6358  oav2  6359  omv2  6361  eqer  6461  ecelqsg  6482  elqsn0m  6497  qsel  6506  qliftf  6514  ecoptocl  6516  eroprf  6522  ecopovsym  6525  ecopovtrn  6526  ecopovsymg  6528  ecopovtrng  6529  th3qlem2  6532  th3q  6534  mapsncnv  6589  mapsnf1o3  6591  mptelixpg  6628  ixpsnf1o  6630  en2d  6662  en3d  6663  dom2lem  6666  dom2  6669  1domsn  6713  xpcomen  6721  xpf1o  6738  mapxpen  6742  fidifsnen  6764  isbth  6855  elfir  6861  supsnti  6892  djueq1  6925  djueq2  6926  djuf1olem  6938  inl11  6950  updjud  6967  omp1eom  6980  difinfsn  6985  ctmlemr  6993  ctssdclemn0  6995  ctssdclemr  6997  ctssdc  6998  enumct  7000  nnnninf  7023  ismkvnex  7029  mkvprop  7032  exmidonfin  7050  exmidaclem  7064  exmidac  7065  cc3  7083  0npi  7128  indpi  7157  recidnq  7208  addnnnq0  7264  mulnnnq0  7265  genpprecll  7329  genppreclu  7330  caucvgprpr  7527  addsrpr  7560  mulsrpr  7561  0nsr  7564  00sr  7584  caucvgsrlemgt1  7610  opelreal  7642  eqresr  7651  axprecex  7695  nntopi  7709  axpre-suploc  7717  ltxrlt  7837  pncan3  7977  apreim  8372  divcanap2  8447  divcanap3  8465  lble  8712  sup3exmid  8722  nn1gt1  8761  0nn0  8999  pnf0xnn0  9054  0z  9072  decaddm10  9247  decmulnc  9255  10p10e20  9283  4t4e16  9287  5t4e20  9290  6t3e18  9293  6t4e24  9294  6t5e30  9295  7t3e21  9298  7t4e28  9299  7t5e35  9300  7t6e42  9301  7t7e49  9302  8t3e24  9304  8t4e32  9305  8t5e40  9306  8t7e56  9308  8t8e64  9309  9t3e27  9311  9t4e36  9312  9t5e45  9313  9t6e54  9314  9t7e63  9315  9t8e72  9316  9t9e81  9317  infrenegsupex  9396  znq  9423  ltpnf  9574  mnflt  9576  mnfltpnf  9578  xnegpnf  9618  xnegmnf  9619  xaddpnf1  9636  xaddpnf2  9637  xaddmnf1  9638  xaddmnf2  9639  pnfaddmnf  9640  mnfaddpnf  9641  lincmb01cmp  9793  iccf1o  9794  elfzuz2  9816  fseq1m1p1  9882  fz0tp  9908  flqdiv  10101  frec2uzzd  10180  frec2uzsucd  10181  frecuzrdgrrn  10188  frec2uzrdg  10189  frecuzrdgrcl  10190  frecuzrdgsuc  10194  frecuzrdgrclt  10195  frecuzrdgg  10196  frecuzrdgsuctlem  10203  uzenom  10205  fzfig  10210  nnenom  10214  seqeq1  10228  seq3val  10238  seqvalcd  10239  seqf  10241  seq3p1  10242  seqovcd  10243  seqp1cd  10246  seq3feq2  10250  seq3feq  10252  monoord2  10257  ser3mono  10258  seq3split  10259  seq3caopr2  10262  iseqf1olemqk  10274  seq3f1olemqsumkj  10278  seq3f1olemstep  10281  seq3f1oleml  10283  seq3f1o  10284  seq3homo  10290  seq3z  10291  seqfeq3  10292  seq3distr  10293  ser0f  10295  ser3ge0  10297  ser3le  10298  exp0  10304  0exp  10335  sq0  10390  sq10  10466  sq10e99m1  10467  facnn  10480  fac0  10481  bcval5  10516  hashinfom  10531  hashennn  10533  hashcl  10534  hashfz1  10536  hashen  10537  hash0  10550  fihashdom  10556  hashun  10558  seq3coll  10592  shftfibg  10599  shftfib  10602  shftfn  10603  2shfti  10610  seq3shft  10617  cvg1n  10765  resqrexlemsqa  10803  negfi  11006  xrmaxiflemcom  11025  xrmaxif  11027  infxrnegsupex  11039  climconst2  11067  climres  11079  climshft  11080  serclim0  11081  climle  11110  clim2ser  11113  clim2ser2  11114  climub  11120  climcvg1n  11126  climcaucn  11127  serf0  11128  sumfct  11150  fsum3cvg  11154  summodclem2  11158  zsumdc  11160  fsum3  11163  isumz  11165  fsumf1o  11166  isumss  11167  fsum3cvg2  11170  fsumsersdc  11171  fsum3ser  11173  fsumcl2lem  11174  fsumadd  11182  fsumsplitf  11184  sumsnf  11185  isummulc2  11202  isumadd  11207  fsumcnv  11213  mptfzshft  11218  fsumrev  11219  fsumshft  11220  fsummulc2  11224  iserabs  11251  isumshft  11266  isum1p  11268  isumlessdc  11272  divcnv  11273  trireciplem  11276  trirecip  11277  expcnvap0  11278  expcnvre  11279  expcnv  11280  explecnv  11281  geolim  11287  geolim2  11288  geo2lim  11292  geoisum  11293  geoisumr  11294  geoisum1  11295  geoisum1c  11296  cvgratnnlemseq  11302  cvgratz  11308  mertenslemub  11310  mertenslemi1  11311  mertenslem2  11312  mertensabs  11313  clim2prod  11315  clim2divap  11316  prodfap0  11321  prodfrecap  11322  prodfdivap  11323  prodeq2w  11332  fproddccvg  11348  prodmodclem2  11353  efcllemp  11371  efval  11374  eff  11376  efcvgfsum  11380  reefcl  11381  ege2le3  11384  ef0  11385  efcj  11386  efaddlem  11387  efadd  11388  eftlcl  11401  reeftlcl  11402  eftlub  11403  efsep  11404  effsumlt  11405  efgt1p2  11408  efgt1p  11409  eflegeo  11415  ef01bndlem  11470  sin01bnd  11471  cos01bnd  11472  eirraplem  11490  eirrap  11491  egt2lt3  11493  dvdsmul2  11523  odd2np1lem  11576  gcd0val  11656  gcd0id  11674  bezoutlemnewy  11691  eucalgcvga  11746  eucalg  11747  lcm0val  11753  qnumdencoprm  11878  qeqnumdivden  11879  phimul  11909  hashgcdeq  11911  xpnnen  11914  ennnfonelemk  11920  ennnfonelemj0  11921  ennnfonelem0  11925  ennnfonelemnn0  11942  ctinfom  11948  ctiunct  11960  ressid  12030  2strstr1g  12072  srngstrd  12091  ipsstrd  12110  elrest  12137  elrestr  12138  topnpropgd  12144  toptopon2  12196  toponmax  12202  tpstop  12212  tpspropd  12213  tsettps  12215  eltpsg  12217  tgiun  12252  ntrval  12289  clsval  12290  0cld  12291  uncld  12292  cldcls  12293  ntr0  12313  isopn3i  12314  neif  12320  neival  12322  neii2  12328  neiss  12329  opnneiss  12337  innei  12342  neissex  12344  tgrest  12348  stoig  12352  restco  12353  resttopon2  12357  restopn2  12362  cnpval  12377  cntop1  12380  cntop2  12381  cnprcl2k  12385  lmcvg  12396  iscnp4  12397  cnima  12399  cnco  12400  cnclima  12402  cnntri  12403  cnntr  12404  cnss1  12405  cnss2  12406  cncnpi  12407  cncnp  12409  cnrest  12414  cnrest2  12415  cnrest2r  12416  lmss  12425  lmres  12427  lmcn  12430  txuni2  12435  txbasex  12436  eltx  12438  txtop  12439  txtopon  12441  txopn  12444  txss12  12445  txbasval  12446  neitx  12447  txcnp  12450  upxp  12451  txcnmpt  12452  uptx  12453  txcn  12454  txrest  12455  txdis1cn  12457  txlm  12458  lmcn2  12459  cnmpt11  12462  cnmpt11f  12463  cnmpt1t  12464  cnmpt12  12466  cnmpt21  12470  cnmpt21f  12471  cnmpt2t  12472  cnmpt22  12473  cnmpt1res  12475  cnmpt2res  12476  cnmptcom  12477  imasnopn  12478  hmeocnv  12486  hmeoopn  12490  hmeocld  12491  hmeontr  12492  hmeoimaf1o  12493  hmeores  12494  txhmeo  12498  txswaphmeo  12500  xmet0  12542  blfvalps  12564  blfps  12588  blf  12589  blpnfctr  12618  xmetresbl  12619  isxms2  12631  xmstps  12636  msxms  12637  xmsxmet  12639  msmet  12640  xmspropd  12656  mspropd  12657  neibl  12670  bdxmet  12680  bdmopn  12683  mopnex  12684  xmetxp  12686  xmettxlem  12688  xmettx  12689  txmetcnp  12697  metcnpd  12699  cnmet  12709  unicntopcntop  12715  cnopncntop  12716  remetdval  12718  resubmet  12727  tgioo2cntop  12728  addcncntoplem  12730  divcnap  12734  fsumcncntop  12735  divccncfap  12756  cncfmet  12758  cncfcncntop  12759  cncfmptc  12761  cncfmptid  12762  cncfmpt1f  12763  cncfmpt2fcntop  12764  cdivcncfap  12766  negfcncf  12768  mulcncflem  12769  mulcncf  12770  cnopnap  12773  ivthinc  12800  ivthdec  12801  limcmpted  12811  limcimolemlt  12812  cnplimcim  12815  cnplimclemr  12817  cnlimcim  12819  cnlimc  12820  cnmptlimc  12822  limccnpcntop  12823  limccnp2lem  12824  limccnp2cntop  12825  reldvg  12827  dvfvalap  12829  dvcl  12831  dvbss  12833  dvfgg  12836  dvidlemap  12839  dvcnp2cntop  12842  dvcn  12843  dvaddxxbr  12844  dvmulxxbr  12845  dvaddxx  12846  dvmulxx  12847  dviaddf  12848  dvimulf  12849  dvcoapbr  12850  dvcjbr  12851  dvrecap  12856  dveflem  12865  dvef  12866  sincn  12868  coscn  12869  ex-or  12944  ex-an  12945  1kp2ke3k  12946  ex-exp  12949  ex-fac  12950  bj-2inf  13146  bj-inf2vnlem1  13178  subctctexmid  13206  nnsf  13209  peano3nninf  13211  nninfalllemn  13212  nninfself  13219  nninfsellemeqinf  13222  nninffeq  13226  trilpolemcl  13240  trilpolemisumle  13241  trilpolemeq1  13243  trilpolemlt1  13244