Theorem eqid 2177

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

Syntax hints:   = wceq 1353   ∈ wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  eqidd  2178  neirr  2356  sbsbc  2966  sbceqal  3018  dfnul2  3424  snidg  3621  prid1g  3696  tpid1  3703  tpid1g  3704  tpid2  3705  tpid2g  3706  tpid3  3708  dfiin2g  3919  eqbrtrid  4038  eqbrtrrid  4039  breqtrdi  4044  opabbii  4070  mpteq2ia  4089  mpteq2da  4092  sucidg  4416  onsucelsucexmidlem1  4527  regexmidlemm  4531  regexmidlem1  4532  reg2exmidlema  4533  regexmid  4534  reg2exmid  4535  reg3exmid  4579  tfisi  4586  finds1  4601  nn0suc  4603  nndceq0  4617  0elnn  4618  nnregexmid  4620  opelxp  4656  relopab  4753  relop  4777  ididg  4780  elrnmpt1s  4877  dfiun3g  4884  dfiin3g  4885  dmmptg  5126  funfn  5246  mpt0  5343  f0  5406  dffn4  5444  f1orn  5471  f1oabexg  5473  f1o00  5496  f1o0  5498  fnbrfvb  5556  fnrnfv  5562  funfvdm  5579  fvmptg  5592  fvmptd  5597  fvmpt2d  5602  fvmptdf  5603  mpteqb  5606  fvmptt  5607  fnmptfvd  5620  funfvop  5628  eldmrexrn  5657  fvmptelcdm  5669  fmpttd  5671  fmpt2d  5678  fmptco  5682  fmptcof  5683  fnasrn  5694  fnasrng  5696  mptexg  5741  eufnfv  5747  idref  5757  f1elima  5773  fliftrel  5792  fliftel  5793  fliftel1  5794  fliftcnv  5795  fliftf  5799  riotabiia  5847  acexmidlem2  5871  acexmidlemv  5872  oprabbii  5929  mpoeq12  5934  ovmpodxf  5999  ovmpodf  6005  ov6g  6011  f1ocnvd  6072  f1opw2  6076  suppssfv  6078  suppssov1  6079  ofvalg  6091  off  6094  offval2  6097  ofrfval2  6098  caofinvl  6104  mptexw  6113  abrexex  6117  abrexexg  6118  offres  6135  ofmres  6136  op1steq  6179  reldm  6186  mpoexga  6212  mpoexw  6213  mpoex  6214  fnmpoovd  6215  fmpoco  6216  cnvf1o  6225  f1od2  6235  tposssxp  6249  brtpos2  6251  tpos0  6274  iunon  6284  tfrfun  6320  tfr2a  6321  tfrlemisucfn  6324  tfri1d  6335  tfr1onlemsucfn  6340  tfr1onlemubacc  6346  tfr1on  6350  tfri1dALT  6351  tfrcllemubacc  6359  tfrex  6368  rdgfun  6373  rdgon  6386  rdg0  6387  frec0g  6397  frecfnom  6401  freccllem  6402  freccl  6403  frecfcllem  6404  frecfcl  6405  frecsuclem  6406  0lt1o  6440  oafnex  6444  omfnex  6449  fnoei  6452  oeiexg  6453  oeiv  6456  oacl  6460  omcl  6461  oeicl  6462  oav2  6463  omv2  6465  eqer  6566  ecelqsg  6587  elqsn0m  6602  qsel  6611  qliftf  6619  ecoptocl  6621  eroprf  6627  ecopovsym  6630  ecopovtrn  6631  ecopovsymg  6633  ecopovtrng  6634  th3qlem2  6637  th3q  6639  mapsncnv  6694  mapsnf1o3  6696  mptelixpg  6733  ixpsnf1o  6735  en2d  6767  en3d  6768  dom2lem  6771  dom2  6774  1domsn  6818  xpcomen  6826  xpf1o  6843  mapxpen  6847  fidifsnen  6869  isbth  6965  elfir  6971  supsnti  7003  djueq1  7038  djueq2  7039  djuf1olem  7051  inl11  7063  updjud  7080  omp1eom  7093  difinfsn  7098  ctmlemr  7106  ctssdclemn0  7108  ctssdclemr  7110  ctssdc  7111  enumct  7113  infnninf  7121  nnnninf  7123  nnnninfeq  7125  nninfisollemne  7128  nninfisol  7130  ismkvnex  7152  mkvprop  7155  nninfwlporlemd  7169  nninfwlpoimlemginf  7173  exmidonfin  7192  exmidaclem  7206  exmidac  7207  cc3  7266  0npi  7311  indpi  7340  recidnq  7391  addnnnq0  7447  mulnnnq0  7448  genpprecll  7512  genppreclu  7513  caucvgprpr  7710  addsrpr  7743  mulsrpr  7744  0nsr  7747  00sr  7767  caucvgsrlemgt1  7793  opelreal  7825  eqresr  7834  axprecex  7878  nntopi  7892  axpre-suploc  7900  ltxrlt  8022  pncan3  8164  apreim  8559  divcanap2  8636  divcanap3  8654  lble  8903  sup3exmid  8913  nn1gt1  8952  0nn0  9190  pnf0xnn0  9245  0z  9263  decaddm10  9441  decmulnc  9449  10p10e20  9477  4t4e16  9481  5t4e20  9484  6t3e18  9487  6t4e24  9488  6t5e30  9489  7t3e21  9492  7t4e28  9493  7t5e35  9494  7t6e42  9495  7t7e49  9496  8t3e24  9498  8t4e32  9499  8t5e40  9500  8t7e56  9502  8t8e64  9503  9t3e27  9505  9t4e36  9506  9t5e45  9507  9t6e54  9508  9t7e63  9509  9t8e72  9510  9t9e81  9511  infrenegsupex  9593  znq  9623  ltpnf  9779  mnflt  9782  mnfltpnf  9784  xnegpnf  9827  xnegmnf  9828  xaddpnf1  9845  xaddpnf2  9846  xaddmnf1  9847  xaddmnf2  9848  pnfaddmnf  9849  mnfaddpnf  9850  lincmb01cmp  10002  iccf1o  10003  iccen  10005  elfzuz2  10028  fseq1m1p1  10094  fz0tp  10121  fz0to4untppr  10123  flqdiv  10320  frec2uzzd  10399  frec2uzsucd  10400  frecuzrdgrrn  10407  frec2uzrdg  10408  frecuzrdgrcl  10409  frecuzrdgsuc  10413  frecuzrdgrclt  10414  frecuzrdgg  10415  frecuzrdgsuctlem  10422  uzenom  10424  fzfig  10429  nnenom  10433  seqeq1  10447  seq3val  10457  seqvalcd  10458  seqf  10460  seq3p1  10461  seqovcd  10462  seqp1cd  10465  seq3feq2  10469  seq3feq  10471  monoord2  10476  ser3mono  10477  seq3split  10478  seq3caopr2  10481  iseqf1olemqk  10493  seq3f1olemqsumkj  10497  seq3f1olemstep  10500  seq3f1oleml  10502  seq3f1o  10503  seq3homo  10509  seq3z  10510  seqfeq3  10511  seq3distr  10512  ser0f  10514  ser3ge0  10516  ser3le  10517  exp0  10523  0exp  10554  sq0  10610  sq10  10691  sq10e99m1  10692  facnn  10706  fac0  10707  bcval5  10742  hashinfom  10757  hashennn  10759  hashcl  10760  hashfz1  10762  hashen  10763  hash0  10775  fihashdom  10782  hashun  10784  seq3coll  10821  shftfibg  10828  shftfib  10831  shftfn  10832  2shfti  10839  seq3shft  10846  cvg1n  10994  resqrexlemsqa  11032  negfi  11235  xrmaxiflemcom  11256  xrmaxif  11258  infxrnegsupex  11270  climconst2  11298  climres  11310  climshft  11311  serclim0  11312  climle  11341  clim2ser  11344  clim2ser2  11345  climub  11351  climcvg1n  11357  climcaucn  11358  serf0  11359  sumfct  11381  fsum3cvg  11385  summodclem2  11389  zsumdc  11391  fsum3  11394  isumz  11396  fsumf1o  11397  isumss  11398  fsum3cvg2  11401  fsumsersdc  11402  fsum3ser  11404  fsumcl2lem  11405  fsumadd  11413  fsumsplitf  11415  sumsnf  11416  isummulc2  11433  isumadd  11438  fsumcnv  11444  mptfzshft  11449  fsumrev  11450  fsumshft  11451  fsummulc2  11455  iserabs  11482  isumshft  11497  isum1p  11499  isumlessdc  11503  divcnv  11504  trireciplem  11507  trirecip  11508  expcnvap0  11509  expcnvre  11510  expcnv  11511  explecnv  11512  geolim  11518  geolim2  11519  geo2lim  11523  geoisum  11524  geoisumr  11525  geoisum1  11526  geoisum1c  11527  cvgratnnlemseq  11533  cvgratz  11539  mertenslemub  11541  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  clim2prod  11546  clim2divap  11547  prodfap0  11552  prodfrecap  11553  prodfdivap  11554  prodeq2w  11563  fproddccvg  11579  prodmodclem2  11584  zproddc  11586  fprodseq  11590  fprodntrivap  11591  prod1dc  11593  prodfct  11594  fprodf1o  11595  prodssdc  11596  fprodssdc  11597  fprodmul  11598  prodsnf  11599  fprodshft  11625  fprodrev  11626  fprodcnv  11632  efcllemp  11665  efval  11668  eff  11670  efcvgfsum  11674  reefcl  11675  ege2le3  11678  ef0  11679  efcj  11680  efaddlem  11681  efadd  11682  eftlcl  11695  reeftlcl  11696  eftlub  11697  efsep  11698  effsumlt  11699  efgt1p2  11702  efgt1p  11703  eflegeo  11708  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  eirraplem  11783  eirrap  11784  egt2lt3  11786  dvdsmul2  11820  odd2np1lem  11876  nninfdcex  11953  zsupssdc  11954  gcd0val  11960  gcd0id  11979  bezoutlemnewy  11996  nnmindc  12034  nnminle  12035  eucalgcvga  12057  eucalg  12058  lcm0val  12064  qnumdencoprm  12192  qeqnumdivden  12193  phimul  12225  eulerthlemh  12230  eulerthlemth  12231  prmdivdiv  12236  hashgcdeq  12238  phisum  12239  odzval  12240  powm2modprm  12251  reumodprminv  12252  pythagtriplem18  12280  pcpremul  12292  pceulem  12293  pceu  12294  pczpre  12296  pczcl  12297  pcmul  12300  pcdiv  12301  pc1  12304  pczdvds  12312  pczndvds  12314  pczndvds2  12316  pcneg  12323  infpn  12358  1arithlem2  12361  1arith  12364  4sqlem3  12387  mul4sq  12391  xpnnen  12394  ennnfonelemk  12400  ennnfonelemj0  12401  ennnfonelem0  12405  ennnfonelemnn0  12422  ctinfom  12428  ctiunct  12440  ssnnct  12447  nninfdclemcl  12448  nninfdclemf  12449  nninfdclemp1  12450  2strstr1g  12579  ressplusgd  12586  srngstrd  12603  ipsstrd  12633  elrest  12694  elrestr  12695  topnpropgd  12701  imasbas  12727  imasplusg  12728  imasmulr  12729  qusin  12745  qusbas  12746  qusaddval  12753  qusaddf  12754  qusmulval  12755  qusmulf  12756  mgmsscl  12779  plusffng  12783  mgmplusf  12784  mgmb1mgm1  12786  mgm0  12787  mgm1  12788  opifismgmdc  12789  grpidpropdg  12792  0g0  12794  mgmidcl  12796  mgmlrid  12797  grpidd  12801  sgrpmgm  12812  sgrp0  12814  sgrp1  12815  sgrpidmndm  12820  mndsgrp  12821  mndidcl  12830  mndbn0  12831  hashfinmndnn  12832  ismndd  12837  mndpfo  12838  mndfo  12839  mndpropd  12840  issubmnd  12842  ress0g  12843  mnd1  12846  mhmf  12855  mhmpropd  12856  mhmlin  12857  mhm0  12858  idmhm  12859  mhmf1o  12860  issubm2  12863  mndissubm  12865  submss  12866  submid  12867  subm0cl  12868  submcl  12869  0subm  12870  insubm  12871  0mhm  12872  mhmco  12873  mhmima  12874  mhmeql  12875  grpmnd  12883  grppropd  12892  isgrpd2e  12895  dfgrp2  12901  grpbn0  12904  grpn0  12907  grprcan  12909  grpidd2  12913  grpinvval  12915  grpinvfng  12916  grpsubval  12918  grpinvf  12919  grplrinv  12926  grpidinv  12928  grpinvid  12929  grpressid  12930  grplcan  12931  grpasscan1  12932  grpasscan2  12933  grpinvinv  12936  grpinvcnv  12937  grplmulf1o  12943  grpinvpropdg  12944  grpidssd  12945  grpinvssd  12946  grpinvadd  12947  grpsubf  12948  grpsubrcan  12950  grpinvsub  12951  grpinvval2  12952  grpsubid  12953  grpsubid1  12954  grpsubeq0  12955  grpsubadd0sub  12956  grpsubadd  12957  grpsubsub  12958  grpaddsubass  12959  grppncan  12960  grpnpcan  12961  grpnnncan2  12966  dfgrp3m  12968  grplactcnv  12971  grplactf1o  12972  grpsubpropdg  12973  grpsubpropd2  12974  grp1  12975  grp1inv  12976  mhmid  12978  mhmmnd  12979  mhmfmhm  12980  ghmgrp  12981  mulgfng  12986  mulg0  12987  mulgnn  12988  mulg1  12989  mulgnnp1  12990  mulgnegnn  12992  mulgnn0p1  12993  mulgnnsubcl  12994  mulgnncl  12997  mulgnn0cl  12998  mulgcl  12999  mulgneg  13000  mulgaddcomlem  13004  mulgaddcom  13005  mulginvcom  13006  mulgnn0z  13008  mulgz  13009  mulgnndir  13010  mulgnn0dir  13011  mulgdirlem  13012  mulgdir  13013  mulgneg2  13015  mulgnnass  13016  mulgnn0ass  13017  mulgass  13018  mulgmodid  13020  mulgsubdir  13021  mhmmulg  13022  mulgpropdg  13023  submmulgcl  13024  subggrp  13035  subgbas  13036  subgrcl  13037  subg0  13038  subginv  13039  subg0cl  13040  subginvcl  13041  subgcl  13042  subgsubcl  13043  subgsub  13044  subgmulgcl  13045  subgmulg  13046  issubg2m  13047  issubgrpd2  13048  issubgrpd  13049  issubg3  13050  issubg4m  13051  grpissubg  13052  subgsubm  13054  subsubg  13055  subgintm  13056  0subg  13057  nsgsubg  13063  isnsg3  13065  nmzsubg  13068  ssnmz  13069  nmznsg  13071  0nsg  13072  nsgid  13073  eqgval  13080  eqger  13081  eqglact  13082  eqgid  13083  eqgen  13084  eqgcpbl  13085  cmnpropd  13096  iscmnd  13099  cmnmnd  13102  ablsub2inv  13112  ablsub4  13114  abladdsub4  13115  ablpncan2  13117  ablsubsub4  13120  ablpnpcan  13121  ablnncan  13122  ablsub32  13123  ablnnncan  13124  ablsubsub23  13126  subcmnd  13127  mgpex  13133  mgpbasg  13134  mgpscag  13135  mgptsetg  13136  mgptopng  13137  mgpdsg  13138  mgpress  13139  dfur2g  13143  srgcmn  13147  srgmgp  13149  srgdilem  13150  srgcl  13151  srgass  13152  srgideu  13153  srgidcl  13157  srgidmlem  13159  issrgid  13162  srgrz  13165  srglz  13166  srg1zr  13168  srgmulgass  13170  srgpcomp  13171  srgpcompp  13172  srgpcomppsc  13173  srglmhm  13174  srgrmhm  13175  srg1expzeq1  13176  ringgrp  13182  ringmgp  13183  crngring  13189  mgpf  13192  ringdilem  13193  ringcl  13194  crngcom  13195  iscrng2  13196  ringass  13197  ringideu  13198  ringidcl  13201  ringidmlem  13203  isringid  13206  ringid  13207  ringidss  13210  ringcom  13212  ringabl  13213  ringpropd  13215  crngpropd  13216  isringd  13218  iscrngd  13219  ringlz  13220  ringrz  13221  ringsrg  13222  ring1eq0  13223  ringnegl  13226  rngnegr  13227  ringmneg1  13228  ringmneg2  13229  ringsubdi  13231  rngsubdir  13232  mulgass2  13233  ring1  13234  ringn0  13235  ringressid  13236  opprex  13243  opprsllem  13244  opprring  13247  opprringbg  13248  oppr0g  13249  oppr1g  13250  opprnegg  13251  mulgass3  13252  reldvdsrsrg  13259  dvdsrvald  13260  dvdsrd  13261  dvdsrmuld  13263  dvdsrex  13265  dvdsrcl2  13266  dvdsrid  13267  dvdsrtr  13268  dvdsrneg  13270  dvdsr01  13271  dvdsr02  13272  1unit  13274  opprunitd  13277  crngunit  13278  dvdsunit  13279  unitmulcl  13280  unitmulclb  13281  unitgrpbasd  13282  unitgrp  13283  unitabl  13284  unitgrpid  13285  unitsubm  13286  invrfvald  13289  unitinvcl  13290  unitinvinv  13291  unitlinv  13293  unitrinv  13294  1rinv  13295  0unit  13296  unitnegcl  13297  dvrvald  13301  dvrcl  13302  unitdvcl  13303  dvrid  13304  dvr1  13305  dvrass  13306  dvrcan1  13307  dvrcan3  13308  dvreq1  13309  dvrdir  13310  rdivmuldivd  13311  ringinvdv  13312  rngidpropdg  13313  unitpropdg  13315  invrpropdg  13316  ringelnzr  13326  nzrunit  13327  lringuplu  13335  subrgss  13341  subrgid  13342  subrgring  13343  subrgcrng  13344  subrgrcl  13345  subrgsubg  13346  subrg1cl  13348  subrg1  13350  subrgmcl  13352  subrgsubm  13353  subrgdvds  13354  subrguss  13355  subrginv  13356  subrgdv  13357  subrgunit  13358  subrgugrp  13359  issubrg2  13360  subrgnzr  13361  subrgintm  13362  subsubrg  13364  issubrg3  13366  subrgpropd  13367  aprirr  13371  aprsym  13372  aprcotr  13373  aprap  13374  islmodd  13381  lmodgrp  13382  lmodring  13383  lmodvscl  13393  scaffng  13397  lmodscaf  13398  lmodvsdi  13399  lmodvsdir  13400  lmodvsass  13401  lmodvs1  13404  cnfld0  13435  cnfld1  13436  cnfldneg  13437  cnfldplusf  13438  cnfldsub  13439  cnfldmulg  13440  cnfldexp  13441  cnsubglem  13443  zsssubrg  13449  zringmulg  13458  zringinvg  13464  zringmpg  13466  toptopon2  13489  toponmax  13495  tpstop  13505  tpspropd  13506  tsettps  13508  eltpsg  13510  tgiun  13543  ntrval  13580  clsval  13581  0cld  13582  uncld  13583  cldcls  13584  ntr0  13604  isopn3i  13605  neif  13611  neival  13613  neii2  13619  neiss  13620  opnneiss  13628  innei  13633  neissex  13635  tgrest  13639  stoig  13643  restco  13644  resttopon2  13648  restopn2  13653  cnpval  13668  cntop1  13671  cntop2  13672  cnprcl2k  13676  lmcvg  13687  iscnp4  13688  cnima  13690  cnco  13691  cnclima  13693  cnntri  13694  cnntr  13695  cnss1  13696  cnss2  13697  cncnpi  13698  cncnp  13700  cnrest  13705  cnrest2  13706  cnrest2r  13707  lmss  13716  lmres  13718  lmcn  13721  txuni2  13726  txbasex  13727  eltx  13729  txtop  13730  txtopon  13732  txopn  13735  txss12  13736  txbasval  13737  neitx  13738  txcnp  13741  upxp  13742  txcnmpt  13743  uptx  13744  txcn  13745  txrest  13746  txdis1cn  13748  txlm  13749  lmcn2  13750  cnmpt11  13753  cnmpt11f  13754  cnmpt1t  13755  cnmpt12  13757  cnmpt21  13761  cnmpt21f  13762  cnmpt2t  13763  cnmpt22  13764  cnmpt1res  13766  cnmpt2res  13767  cnmptcom  13768  imasnopn  13769  hmeocnv  13777  hmeoopn  13781  hmeocld  13782  hmeontr  13783  hmeoimaf1o  13784  hmeores  13785  txhmeo  13789  txswaphmeo  13791  xmet0  13833  blfvalps  13855  blfps  13879  blf  13880  blpnfctr  13909  xmetresbl  13910  isxms2  13922  xmstps  13927  msxms  13928  xmsxmet  13930  msmet  13931  xmspropd  13947  mspropd  13948  neibl  13961  bdxmet  13971  bdmopn  13974  mopnex  13975  xmetxp  13977  xmettxlem  13979  xmettx  13980  txmetcnp  13988  metcnpd  13990  cnmet  14000  unicntopcntop  14006  cnopncntop  14007  remetdval  14009  resubmet  14018  tgioo2cntop  14019  addcncntoplem  14021  divcnap  14025  fsumcncntop  14026  divccncfap  14047  cncfmet  14049  cncfcncntop  14050  cncfmptc  14052  cncfmptid  14053  cncfmpt1f  14054  cncfmpt2fcntop  14055  cdivcncfap  14057  negfcncf  14059  mulcncflem  14060  mulcncf  14061  cnopnap  14064  ivthinc  14091  ivthdec  14092  limcmpted  14102  limcimolemlt  14103  cnplimcim  14106  cnplimclemr  14108  cnlimcim  14110  cnlimc  14111  cnmptlimc  14113  limccnpcntop  14114  limccnp2lem  14115  limccnp2cntop  14116  reldvg  14118  dvfvalap  14120  dvcl  14122  dvbss  14124  dvfgg  14127  dvidlemap  14130  dvcnp2cntop  14133  dvcn  14134  dvaddxxbr  14135  dvmulxxbr  14136  dvaddxx  14137  dvmulxx  14138  dviaddf  14139  dvimulf  14140  dvcoapbr  14141  dvcjbr  14142  dvrecap  14147  dveflem  14157  dvef  14158  sincn  14160  coscn  14161  lgsfcl  14379  lgsfle1  14380  lgsval4lem  14382  lgscl2  14383  lgs0  14384  lgscl  14385  lgsle1  14386  lgsval2  14387  lgs2  14388  lgsval4  14391  lgsfcl3  14392  lgsneg  14395  lgsmod  14397  lgsdirprm  14405  lgsdir  14406  lgsdi  14408  lgsne0  14409  2sqlem9  14441  ex-or  14444  ex-an  14445  1kp2ke3k  14446  ex-exp  14449  ex-fac  14450  fnmptd  14526  bj-2inf  14660  bj-inf2vnlem1  14692  subctctexmid  14720  nnsf  14724  peano3nninf  14726  nninfself  14732  nninfsellemeqinf  14735  nninffeq  14739  iooreen  14753  trilpolemcl  14755  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  iswomni0  14769  dceqnconst  14777  dcapnconst  14778  nconstwlpolemgt0  14781