Theorem eqid 2165

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

Syntax hints:   = wceq 1343   ∈ wcel 2136

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 1437  ax-ext 2147

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

This theorem is referenced by:  eqidd  2166  neirr  2345  sbsbc  2955  sbceqal  3006  dfnul2  3411  snidg  3605  prid1g  3680  tpid1  3687  tpid1g  3688  tpid2  3689  tpid2g  3690  tpid3  3692  dfiin2g  3899  eqbrtrid  4017  eqbrtrrid  4018  breqtrdi  4023  opabbii  4049  mpteq2ia  4068  mpteq2da  4071  sucidg  4394  onsucelsucexmidlem1  4505  regexmidlemm  4509  regexmidlem1  4510  reg2exmidlema  4511  regexmid  4512  reg2exmid  4513  reg3exmid  4557  tfisi  4564  finds1  4579  nn0suc  4581  nndceq0  4595  0elnn  4596  nnregexmid  4598  opelxp  4634  relopab  4731  relop  4754  ididg  4757  elrnmpt1s  4854  dfiun3g  4861  dfiin3g  4862  dmmptg  5101  funfn  5218  mpt0  5315  f0  5378  dffn4  5416  f1orn  5442  f1oabexg  5444  f1o00  5467  f1o0  5469  fnbrfvb  5527  fnrnfv  5533  funfvdm  5549  fvmptg  5562  fvmptd  5567  fvmpt2d  5572  fvmptdf  5573  mpteqb  5576  fvmptt  5577  funfvop  5597  eldmrexrn  5626  fvmptelrn  5638  fmpttd  5640  fmpt2d  5647  fmptco  5651  fmptcof  5652  fnasrn  5663  fnasrng  5665  mptexg  5710  eufnfv  5715  idref  5725  f1elima  5741  fliftrel  5760  fliftel  5761  fliftel1  5762  fliftcnv  5763  fliftf  5767  riotabiia  5815  acexmidlem2  5839  acexmidlemv  5840  oprabbii  5897  mpoeq12  5902  ovmpodxf  5967  ovmpodf  5973  ov6g  5979  f1ocnvd  6040  f1opw2  6044  suppssfv  6046  suppssov1  6047  ofvalg  6059  off  6062  offval2  6065  ofrfval2  6066  caofinvl  6072  mptexw  6081  abrexex  6085  abrexexg  6086  offres  6103  ofmres  6104  op1steq  6147  reldm  6154  mpoexga  6180  mpoexw  6181  mpoex  6182  fnmpoovd  6183  fmpoco  6184  cnvf1o  6193  f1od2  6203  tposssxp  6217  brtpos2  6219  tpos0  6242  iunon  6252  tfrfun  6288  tfr2a  6289  tfrlemisucfn  6292  tfri1d  6303  tfr1onlemsucfn  6308  tfr1onlemubacc  6314  tfr1on  6318  tfri1dALT  6319  tfrcllemubacc  6327  tfrex  6336  rdgfun  6341  rdgon  6354  rdg0  6355  frec0g  6365  frecfnom  6369  freccllem  6370  freccl  6371  frecfcllem  6372  frecfcl  6373  frecsuclem  6374  0lt1o  6408  oafnex  6412  omfnex  6417  fnoei  6420  oeiexg  6421  oeiv  6424  oacl  6428  omcl  6429  oeicl  6430  oav2  6431  omv2  6433  eqer  6533  ecelqsg  6554  elqsn0m  6569  qsel  6578  qliftf  6586  ecoptocl  6588  eroprf  6594  ecopovsym  6597  ecopovtrn  6598  ecopovsymg  6600  ecopovtrng  6601  th3qlem2  6604  th3q  6606  mapsncnv  6661  mapsnf1o3  6663  mptelixpg  6700  ixpsnf1o  6702  en2d  6734  en3d  6735  dom2lem  6738  dom2  6741  1domsn  6785  xpcomen  6793  xpf1o  6810  mapxpen  6814  fidifsnen  6836  isbth  6932  elfir  6938  supsnti  6970  djueq1  7005  djueq2  7006  djuf1olem  7018  inl11  7030  updjud  7047  omp1eom  7060  difinfsn  7065  ctmlemr  7073  ctssdclemn0  7075  ctssdclemr  7077  ctssdc  7078  enumct  7080  infnninf  7088  nnnninf  7090  nnnninfeq  7092  nninfisollemne  7095  nninfisol  7097  ismkvnex  7119  mkvprop  7122  exmidonfin  7150  exmidaclem  7164  exmidac  7165  cc3  7209  0npi  7254  indpi  7283  recidnq  7334  addnnnq0  7390  mulnnnq0  7391  genpprecll  7455  genppreclu  7456  caucvgprpr  7653  addsrpr  7686  mulsrpr  7687  0nsr  7690  00sr  7710  caucvgsrlemgt1  7736  opelreal  7768  eqresr  7777  axprecex  7821  nntopi  7835  axpre-suploc  7843  ltxrlt  7964  pncan3  8106  apreim  8501  divcanap2  8576  divcanap3  8594  lble  8842  sup3exmid  8852  nn1gt1  8891  0nn0  9129  pnf0xnn0  9184  0z  9202  decaddm10  9380  decmulnc  9388  10p10e20  9416  4t4e16  9420  5t4e20  9423  6t3e18  9426  6t4e24  9427  6t5e30  9428  7t3e21  9431  7t4e28  9432  7t5e35  9433  7t6e42  9434  7t7e49  9435  8t3e24  9437  8t4e32  9438  8t5e40  9439  8t7e56  9441  8t8e64  9442  9t3e27  9444  9t4e36  9445  9t5e45  9446  9t6e54  9447  9t7e63  9448  9t8e72  9449  9t9e81  9450  infrenegsupex  9532  znq  9562  ltpnf  9716  mnflt  9719  mnfltpnf  9721  xnegpnf  9764  xnegmnf  9765  xaddpnf1  9782  xaddpnf2  9783  xaddmnf1  9784  xaddmnf2  9785  pnfaddmnf  9786  mnfaddpnf  9787  lincmb01cmp  9939  iccf1o  9940  iccen  9942  elfzuz2  9964  fseq1m1p1  10030  fz0tp  10057  fz0to4untppr  10059  flqdiv  10256  frec2uzzd  10335  frec2uzsucd  10336  frecuzrdgrrn  10343  frec2uzrdg  10344  frecuzrdgrcl  10345  frecuzrdgsuc  10349  frecuzrdgrclt  10350  frecuzrdgg  10351  frecuzrdgsuctlem  10358  uzenom  10360  fzfig  10365  nnenom  10369  seqeq1  10383  seq3val  10393  seqvalcd  10394  seqf  10396  seq3p1  10397  seqovcd  10398  seqp1cd  10401  seq3feq2  10405  seq3feq  10407  monoord2  10412  ser3mono  10413  seq3split  10414  seq3caopr2  10417  iseqf1olemqk  10429  seq3f1olemqsumkj  10433  seq3f1olemstep  10436  seq3f1oleml  10438  seq3f1o  10439  seq3homo  10445  seq3z  10446  seqfeq3  10447  seq3distr  10448  ser0f  10450  ser3ge0  10452  ser3le  10453  exp0  10459  0exp  10490  sq0  10545  sq10  10625  sq10e99m1  10626  facnn  10640  fac0  10641  bcval5  10676  hashinfom  10691  hashennn  10693  hashcl  10694  hashfz1  10696  hashen  10697  hash0  10710  fihashdom  10716  hashun  10718  seq3coll  10755  shftfibg  10762  shftfib  10765  shftfn  10766  2shfti  10773  seq3shft  10780  cvg1n  10928  resqrexlemsqa  10966  negfi  11169  xrmaxiflemcom  11190  xrmaxif  11192  infxrnegsupex  11204  climconst2  11232  climres  11244  climshft  11245  serclim0  11246  climle  11275  clim2ser  11278  clim2ser2  11279  climub  11285  climcvg1n  11291  climcaucn  11292  serf0  11293  sumfct  11315  fsum3cvg  11319  summodclem2  11323  zsumdc  11325  fsum3  11328  isumz  11330  fsumf1o  11331  isumss  11332  fsum3cvg2  11335  fsumsersdc  11336  fsum3ser  11338  fsumcl2lem  11339  fsumadd  11347  fsumsplitf  11349  sumsnf  11350  isummulc2  11367  isumadd  11372  fsumcnv  11378  mptfzshft  11383  fsumrev  11384  fsumshft  11385  fsummulc2  11389  iserabs  11416  isumshft  11431  isum1p  11433  isumlessdc  11437  divcnv  11438  trireciplem  11441  trirecip  11442  expcnvap0  11443  expcnvre  11444  expcnv  11445  explecnv  11446  geolim  11452  geolim2  11453  geo2lim  11457  geoisum  11458  geoisumr  11459  geoisum1  11460  geoisum1c  11461  cvgratnnlemseq  11467  cvgratz  11473  mertenslemub  11475  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  clim2prod  11480  clim2divap  11481  prodfap0  11486  prodfrecap  11487  prodfdivap  11488  prodeq2w  11497  fproddccvg  11513  prodmodclem2  11518  zproddc  11520  fprodseq  11524  fprodntrivap  11525  prod1dc  11527  prodfct  11528  fprodf1o  11529  prodssdc  11530  fprodssdc  11531  fprodmul  11532  prodsnf  11533  fprodshft  11559  fprodrev  11560  fprodcnv  11566  efcllemp  11599  efval  11602  eff  11604  efcvgfsum  11608  reefcl  11609  ege2le3  11612  ef0  11613  efcj  11614  efaddlem  11615  efadd  11616  eftlcl  11629  reeftlcl  11630  eftlub  11631  efsep  11632  effsumlt  11633  efgt1p2  11636  efgt1p  11637  eflegeo  11642  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  eirraplem  11717  eirrap  11718  egt2lt3  11720  dvdsmul2  11754  odd2np1lem  11809  nninfdcex  11886  zsupssdc  11887  gcd0val  11893  gcd0id  11912  bezoutlemnewy  11929  nnmindc  11967  nnminle  11968  eucalgcvga  11990  eucalg  11991  lcm0val  11997  qnumdencoprm  12125  qeqnumdivden  12126  phimul  12158  eulerthlemh  12163  eulerthlemth  12164  prmdivdiv  12169  hashgcdeq  12171  phisum  12172  odzval  12173  powm2modprm  12184  reumodprminv  12185  pythagtriplem18  12213  pcpremul  12225  pceulem  12226  pceu  12227  pczpre  12229  pczcl  12230  pcmul  12233  pcdiv  12234  pc1  12237  pczdvds  12245  pczndvds  12247  pczndvds2  12249  pcneg  12256  infpn  12291  1arithlem2  12294  1arith  12297  4sqlem3  12320  mul4sq  12324  xpnnen  12327  ennnfonelemk  12333  ennnfonelemj0  12334  ennnfonelem0  12338  ennnfonelemnn0  12355  ctinfom  12361  ctiunct  12373  ssnnct  12380  nninfdclemcl  12381  nninfdclemf  12382  nninfdclemp1  12383  ressid  12456  2strstr1g  12498  srngstrd  12517  ipsstrd  12536  elrest  12563  elrestr  12564  topnpropgd  12570  mgmsscl  12592  plusffng  12596  mgmplusf  12597  mgmb1mgm1  12599  mgm0  12600  mgm1  12601  opifismgmdc  12602  grpidpropdg  12605  0g0  12607  mgmidcl  12609  mgmlrid  12610  grpidd  12614  toptopon2  12657  toponmax  12663  tpstop  12673  tpspropd  12674  tsettps  12676  eltpsg  12678  tgiun  12713  ntrval  12750  clsval  12751  0cld  12752  uncld  12753  cldcls  12754  ntr0  12774  isopn3i  12775  neif  12781  neival  12783  neii2  12789  neiss  12790  opnneiss  12798  innei  12803  neissex  12805  tgrest  12809  stoig  12813  restco  12814  resttopon2  12818  restopn2  12823  cnpval  12838  cntop1  12841  cntop2  12842  cnprcl2k  12846  lmcvg  12857  iscnp4  12858  cnima  12860  cnco  12861  cnclima  12863  cnntri  12864  cnntr  12865  cnss1  12866  cnss2  12867  cncnpi  12868  cncnp  12870  cnrest  12875  cnrest2  12876  cnrest2r  12877  lmss  12886  lmres  12888  lmcn  12891  txuni2  12896  txbasex  12897  eltx  12899  txtop  12900  txtopon  12902  txopn  12905  txss12  12906  txbasval  12907  neitx  12908  txcnp  12911  upxp  12912  txcnmpt  12913  uptx  12914  txcn  12915  txrest  12916  txdis1cn  12918  txlm  12919  lmcn2  12920  cnmpt11  12923  cnmpt11f  12924  cnmpt1t  12925  cnmpt12  12927  cnmpt21  12931  cnmpt21f  12932  cnmpt2t  12933  cnmpt22  12934  cnmpt1res  12936  cnmpt2res  12937  cnmptcom  12938  imasnopn  12939  hmeocnv  12947  hmeoopn  12951  hmeocld  12952  hmeontr  12953  hmeoimaf1o  12954  hmeores  12955  txhmeo  12959  txswaphmeo  12961  xmet0  13003  blfvalps  13025  blfps  13049  blf  13050  blpnfctr  13079  xmetresbl  13080  isxms2  13092  xmstps  13097  msxms  13098  xmsxmet  13100  msmet  13101  xmspropd  13117  mspropd  13118  neibl  13131  bdxmet  13141  bdmopn  13144  mopnex  13145  xmetxp  13147  xmettxlem  13149  xmettx  13150  txmetcnp  13158  metcnpd  13160  cnmet  13170  unicntopcntop  13176  cnopncntop  13177  remetdval  13179  resubmet  13188  tgioo2cntop  13189  addcncntoplem  13191  divcnap  13195  fsumcncntop  13196  divccncfap  13217  cncfmet  13219  cncfcncntop  13220  cncfmptc  13222  cncfmptid  13223  cncfmpt1f  13224  cncfmpt2fcntop  13225  cdivcncfap  13227  negfcncf  13229  mulcncflem  13230  mulcncf  13231  cnopnap  13234  ivthinc  13261  ivthdec  13262  limcmpted  13272  limcimolemlt  13273  cnplimcim  13276  cnplimclemr  13278  cnlimcim  13280  cnlimc  13281  cnmptlimc  13283  limccnpcntop  13284  limccnp2lem  13285  limccnp2cntop  13286  reldvg  13288  dvfvalap  13290  dvcl  13292  dvbss  13294  dvfgg  13297  dvidlemap  13300  dvcnp2cntop  13303  dvcn  13304  dvaddxxbr  13305  dvmulxxbr  13306  dvaddxx  13307  dvmulxx  13308  dviaddf  13309  dvimulf  13310  dvcoapbr  13311  dvcjbr  13312  dvrecap  13317  dveflem  13327  dvef  13328  sincn  13330  coscn  13331  lgsfcl  13549  lgsfle1  13550  lgsval4lem  13552  lgscl2  13553  lgs0  13554  lgscl  13555  lgsle1  13556  lgsval2  13557  lgs2  13558  lgsval4  13561  lgsfcl3  13562  lgsneg  13565  lgsmod  13567  lgsdirprm  13575  lgsdir  13576  lgsdi  13578  lgsne0  13579  2sqlem9  13600  ex-or  13603  ex-an  13604  1kp2ke3k  13605  ex-exp  13608  ex-fac  13609  fnmptd  13686  bj-2inf  13820  bj-inf2vnlem1  13852  subctctexmid  13881  nnsf  13885  peano3nninf  13887  nninfself  13893  nninfsellemeqinf  13896  nninffeq  13900  iooreen  13914  trilpolemcl  13916  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  iswomni0  13930  dceqnconst  13938  dcapnconst  13939  nconstwlpolemgt0  13942