Theorem eqid 2081

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 169	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
2	1	eqriv 2078	1 ⊢ 𝐴 = 𝐴

Syntax hints:   = wceq 1284   ∈ wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  eqidd  2082  neirr  2254  sbsbc  2819  sbceqal  2869  dfnul2  3253  snidg  3423  prid1g  3496  tpid1  3503  tpid2  3504  tpid3  3506  dfiin2g  3711  syl5eqbr  3818  syl5eqbrr  3819  syl6breq  3824  opabbii  3845  mpteq2ia  3864  mpteq2da  3867  sucidg  4171  onsucelsucexmidlem1  4271  regexmidlemm  4275  regexmidlem1  4276  reg2exmidlema  4277  regexmid  4278  reg2exmid  4279  reg3exmid  4322  tfisi  4328  finds1  4343  nn0suc  4345  nndceq0  4357  0elnn  4358  nnregexmid  4360  opelxp  4392  relopab  4482  relop  4504  ididg  4507  elrnmpt1s  4602  dfiun3g  4607  dfiin3g  4608  dmmptg  4838  funfn  4951  mpt0  5046  f0  5100  dffn4  5132  f1orn  5156  f1oabexg  5158  f1o00  5181  f1o0  5183  fnbrfvb  5235  fnrnfv  5241  funfvdm  5257  fvmptg  5269  fvmptd  5274  fvmpt2d  5278  fvmptdf  5279  mpteqb  5282  fvmptt  5283  funfvop  5300  eldmrexrn  5329  fmpt2d  5348  fmptco  5351  fmptcof  5352  fnasrn  5362  fnasrng  5364  mptexg  5407  eufnfv  5410  idref  5417  f1elima  5433  fliftrel  5452  fliftel  5453  fliftel1  5454  fliftcnv  5455  fliftf  5459  riotabiia  5505  acexmidlem2  5529  acexmidlemv  5530  oprabbii  5580  mpt2eq12  5585  ovmpt2dxf  5646  ovmpt2df  5652  ov6g  5658  f1ocnvd  5722  f1opw2  5726  suppssfv  5728  suppssov1  5729  fnofval  5741  off  5744  offval2  5746  ofrfval2  5747  caofinvl  5753  abrexex  5764  abrexexg  5765  offres  5782  ofmres  5783  op1steq  5825  reldm  5832  mpt2exga  5855  mpt2ex  5856  fmpt2co  5857  cnvf1o  5866  f1od2  5876  tposssxp  5887  brtpos2  5889  tpos0  5912  iunon  5922  tfr2a  5959  tfrlemisucfn  5961  tfri1d  5972  tfrex  5977  tfrfun  5978  rdgfun  5983  rdg0  5997  frec0g  6006  frecfnom  6009  frecsuclem1  6010  frecsuclemdm  6011  frecsuclem3  6013  0lt1o  6046  oafnex  6047  omfnex  6052  fnoei  6055  oeiexg  6056  oeiv  6059  oacl  6063  omcl  6064  oeicl  6065  oav2  6066  omv2  6068  eqer  6161  ecelqsg  6182  elqsn0m  6197  qsel  6206  qliftf  6214  ecoptocl  6216  eroprf  6222  ecopovsym  6225  ecopovtrn  6226  ecopovsymg  6228  ecopovtrng  6229  th3qlem2  6232  th3q  6234  en2d  6271  en3d  6272  dom2lem  6275  dom2  6278  xpcomen  6324  fidifsnen  6355  supsnti  6418  0npi  6503  indpi  6532  recidnq  6583  addnnnq0  6639  mulnnnq0  6640  genpprecll  6704  genppreclu  6705  caucvgprpr  6902  addsrpr  6922  mulsrpr  6923  0nsr  6926  00sr  6946  caucvgsrlemgt1  6971  opelreal  6996  eqresr  7004  axprecex  7046  nntopi  7060  ltxrlt  7178  pncan3  7316  apreim  7703  divcanap2  7768  divcanap3  7786  lble  8025  nn1gt1  8072  0nn0  8303  0z  8362  decaddm10  8535  decmulnc  8543  10p10e20  8571  4t4e16  8575  5t4e20  8578  6t3e18  8581  6t4e24  8582  6t5e30  8583  7t3e21  8586  7t4e28  8587  7t5e35  8588  7t6e42  8589  7t7e49  8590  8t3e24  8592  8t4e32  8593  8t5e40  8594  8t7e56  8596  8t8e64  8597  9t3e27  8599  9t4e36  8600  9t5e45  8601  9t6e54  8602  9t7e63  8603  9t8e72  8604  9t9e81  8605  infrenegsupex  8682  znq  8709  ltpnf  8856  mnflt  8858  mnfltpnf  8860  xnegpnf  8895  xnegmnf  8896  lincmb01cmp  9025  iccf1o  9026  elfzuz2  9048  fseq1m1p1  9112  fz0tp  9135  flqdiv  9323  frecuzrdgrrn  9410  uzenom  9418  fzfig  9422  nnenom  9426  iseqeq1  9434  iseqeq4  9437  iseqval  9440  iseqfn  9441  iseq1  9442  iseqcl  9443  iseqp1  9445  monoord2  9456  iseqdistr  9470  serile  9474  exp0  9480  0exp  9511  sq0  9566  sq10  9640  sq10e99m1  9641  shftfibg  9708  shftfib  9711  shftfn  9712  2shfti  9719  cvg1n  9872  resqrexlemsqa  9910  negfi  10110  climconst2  10130  climres  10142  climshft  10143  iserclim0  10144  climle  10172  clim2iser  10175  clim2iser2  10176  climub  10182  climcvg1n  10187  climcaucn  10188  serif0  10189  dvdsmul2  10218  odd2np1lem  10271  gcd0val  10352  gcd0id  10370  bezoutlemnewy  10385  eucialgcvga  10440  eucialg  10441  lcm0val  10447  ex-or  10560  ex-an  10561  1kp2ke3k  10562  ex-fac  10565  bj-2inf  10733  bj-inf2vnlem1  10765