Theorem eqid 2100

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

Syntax hints:   = wceq 1299   ∈ wcel 1448

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 1393  ax-ext 2082

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

This theorem is referenced by:  eqidd  2101  neirr  2276  sbsbc  2866  sbceqal  2916  dfnul2  3312  snidg  3501  prid1g  3574  tpid1  3581  tpid1g  3582  tpid2  3583  tpid2g  3584  tpid3  3586  dfiin2g  3793  syl5eqbr  3908  syl5eqbrr  3909  syl6breq  3914  opabbii  3935  mpteq2ia  3954  mpteq2da  3957  sucidg  4276  onsucelsucexmidlem1  4381  regexmidlemm  4385  regexmidlem1  4386  reg2exmidlema  4387  regexmid  4388  reg2exmid  4389  reg3exmid  4432  tfisi  4439  finds1  4454  nn0suc  4456  nndceq0  4469  0elnn  4470  nnregexmid  4472  opelxp  4507  relopab  4604  relop  4627  ididg  4630  elrnmpt1s  4727  dfiun3g  4732  dfiin3g  4733  dmmptg  4972  funfn  5089  mpt0  5186  f0  5249  dffn4  5287  f1orn  5311  f1oabexg  5313  f1o00  5336  f1o0  5338  fnbrfvb  5394  fnrnfv  5400  funfvdm  5416  fvmptg  5429  fvmptd  5434  fvmpt2d  5439  fvmptdf  5440  mpteqb  5443  fvmptt  5444  funfvop  5464  eldmrexrn  5493  fvmptelrn  5505  fmpttd  5507  fmpt2d  5514  fmptco  5518  fmptcof  5519  fnasrn  5530  fnasrng  5532  mptexg  5577  eufnfv  5580  idref  5590  f1elima  5606  fliftrel  5625  fliftel  5626  fliftel1  5627  fliftcnv  5628  fliftf  5632  riotabiia  5679  acexmidlem2  5703  acexmidlemv  5704  oprabbii  5758  mpoeq12  5763  ovmpodxf  5828  ovmpodf  5834  ov6g  5840  f1ocnvd  5904  f1opw2  5908  suppssfv  5910  suppssov1  5911  fnofval  5923  off  5926  offval2  5928  ofrfval2  5929  caofinvl  5935  abrexex  5946  abrexexg  5947  offres  5964  ofmres  5965  op1steq  6007  reldm  6014  mpoexga  6040  mpoex  6041  fnmpoovd  6042  fmpoco  6043  cnvf1o  6052  f1od2  6062  tposssxp  6076  brtpos2  6078  tpos0  6101  iunon  6111  tfrfun  6147  tfr2a  6148  tfrlemisucfn  6151  tfri1d  6162  tfr1onlemsucfn  6167  tfr1onlemubacc  6173  tfr1on  6177  tfri1dALT  6178  tfrcllemubacc  6186  tfrex  6195  rdgfun  6200  rdgon  6213  rdg0  6214  frec0g  6224  frecfnom  6228  freccllem  6229  freccl  6230  frecfcllem  6231  frecfcl  6232  frecsuclem  6233  0lt1o  6267  oafnex  6270  omfnex  6275  fnoei  6278  oeiexg  6279  oeiv  6282  oacl  6286  omcl  6287  oeicl  6288  oav2  6289  omv2  6291  eqer  6391  ecelqsg  6412  elqsn0m  6427  qsel  6436  qliftf  6444  ecoptocl  6446  eroprf  6452  ecopovsym  6455  ecopovtrn  6456  ecopovsymg  6458  ecopovtrng  6459  th3qlem2  6462  th3q  6464  mapsncnv  6519  mapsnf1o3  6521  mptelixpg  6558  ixpsnf1o  6560  en2d  6592  en3d  6593  dom2lem  6596  dom2  6599  1domsn  6642  xpcomen  6650  xpf1o  6667  mapxpen  6671  fidifsnen  6693  isbth  6783  supsnti  6807  djueq1  6840  djueq2  6841  djuf1olem  6853  inl11  6865  updjud  6882  omp1eom  6895  difinfsn  6900  ctmlemr  6908  ctssdclemn0  6910  ctssdc  6912  enumct  6914  nnnninf  6935  mkvprop  6943  0npi  7022  indpi  7051  recidnq  7102  addnnnq0  7158  mulnnnq0  7159  genpprecll  7223  genppreclu  7224  caucvgprpr  7421  addsrpr  7441  mulsrpr  7442  0nsr  7445  00sr  7465  caucvgsrlemgt1  7490  opelreal  7515  eqresr  7523  axprecex  7565  nntopi  7579  ltxrlt  7702  pncan3  7841  apreim  8231  divcanap2  8301  divcanap3  8319  lble  8563  sup3exmid  8573  nn1gt1  8612  0nn0  8844  pnf0xnn0  8899  0z  8917  decaddm10  9092  decmulnc  9100  10p10e20  9128  4t4e16  9132  5t4e20  9135  6t3e18  9138  6t4e24  9139  6t5e30  9140  7t3e21  9143  7t4e28  9144  7t5e35  9145  7t6e42  9146  7t7e49  9147  8t3e24  9149  8t4e32  9150  8t5e40  9151  8t7e56  9153  8t8e64  9154  9t3e27  9156  9t4e36  9157  9t5e45  9158  9t6e54  9159  9t7e63  9160  9t8e72  9161  9t9e81  9162  infrenegsupex  9239  znq  9266  ltpnf  9408  mnflt  9410  mnfltpnf  9412  xnegpnf  9452  xnegmnf  9453  xaddpnf1  9470  xaddpnf2  9471  xaddmnf1  9472  xaddmnf2  9473  pnfaddmnf  9474  mnfaddpnf  9475  lincmb01cmp  9627  iccf1o  9628  elfzuz2  9650  fseq1m1p1  9716  fz0tp  9742  flqdiv  9935  frec2uzzd  10014  frec2uzsucd  10015  frecuzrdgrrn  10022  frec2uzrdg  10023  frecuzrdgrcl  10024  frecuzrdgsuc  10028  frecuzrdgrclt  10029  frecuzrdgg  10030  frecuzrdgsuctlem  10037  uzenom  10039  fzfig  10044  nnenom  10048  seqeq1  10062  seq3val  10072  seqvalcd  10073  seqf  10075  seq3p1  10076  seqovcd  10077  seqp1cd  10080  seq3feq2  10084  seq3feq  10086  monoord2  10091  ser3mono  10092  seq3split  10093  seq3caopr2  10096  iseqf1olemqk  10108  seq3f1olemqsumkj  10112  seq3f1olemstep  10115  seq3f1oleml  10117  seq3f1o  10118  seq3homo  10124  seq3z  10125  seqfeq3  10126  seq3distr  10127  ser0f  10129  ser3ge0  10131  ser3le  10132  exp0  10138  0exp  10169  sq0  10224  sq10  10300  sq10e99m1  10301  facnn  10314  fac0  10315  bcval5  10350  hashinfom  10365  hashennn  10367  hashcl  10368  hashfz1  10370  hashen  10371  hash0  10384  fihashdom  10390  hashun  10392  seq3coll  10426  shftfibg  10433  shftfib  10436  shftfn  10437  2shfti  10444  seq3shft  10451  cvg1n  10598  resqrexlemsqa  10636  negfi  10838  xrmaxiflemcom  10857  xrmaxif  10859  infxrnegsupex  10871  climconst2  10899  climres  10911  climshft  10912  serclim0  10913  climle  10942  clim2ser  10945  clim2ser2  10946  climub  10952  climcvg1n  10958  climcaucn  10959  serf0  10960  sumfct  10982  fsum3cvg  10985  summodclem2  10990  zsumdc  10992  fsum3  10995  isumz  10997  fsumf1o  10998  isumss  10999  fsum3cvg2  11002  fsumsersdc  11003  fsum3ser  11005  fsumcl2lem  11006  fsumadd  11014  fsumsplitf  11016  sumsnf  11017  isummulc2  11034  isumadd  11039  fsumcnv  11045  mptfzshft  11050  fsumrev  11051  fsumshft  11052  fsummulc2  11056  iserabs  11083  isumshft  11098  isum1p  11100  isumlessdc  11104  divcnv  11105  trireciplem  11108  trirecip  11109  expcnvap0  11110  expcnvre  11111  expcnv  11112  explecnv  11113  geolim  11119  geolim2  11120  geo2lim  11124  geoisum  11125  geoisumr  11126  geoisum1  11127  geoisum1c  11128  cvgratnnlemseq  11134  cvgratz  11140  mertenslemub  11142  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  efcllemp  11162  efval  11165  eff  11167  efcvgfsum  11171  reefcl  11172  ege2le3  11175  ef0  11176  efcj  11177  efaddlem  11178  efadd  11179  eftlcl  11192  reeftlcl  11193  eftlub  11194  efsep  11195  effsumlt  11196  efgt1p2  11199  efgt1p  11200  eflegeo  11206  ef01bndlem  11261  sin01bnd  11262  cos01bnd  11263  eirraplem  11278  eirrap  11279  egt2lt3  11281  dvdsmul2  11311  odd2np1lem  11364  gcd0val  11444  gcd0id  11462  bezoutlemnewy  11477  eucalgcvga  11532  eucalg  11533  lcm0val  11539  qnumdencoprm  11663  qeqnumdivden  11664  phimul  11694  hashgcdeq  11696  xpnnen  11699  ennnfonelemk  11705  ennnfonelemj0  11706  ennnfonelem0  11710  ennnfonelemnn0  11727  ctinfom  11733  ressid  11802  2strstr1g  11844  srngstrd  11863  ipsstrd  11882  elrest  11909  elrestr  11910  topnpropgd  11916  toptopon2  11968  toponmax  11974  tpstop  11984  tpspropd  11985  tsettps  11987  eltpsg  11989  tgiun  12024  ntrval  12061  clsval  12062  0cld  12063  uncld  12064  cldcls  12065  ntr0  12085  isopn3i  12086  neif  12092  neival  12094  neii2  12100  neiss  12101  opnneiss  12109  innei  12114  neissex  12116  tgrest  12120  stoig  12124  restco  12125  resttopon2  12129  restopn2  12134  cnpval  12148  cntop1  12151  cntop2  12152  cnprcl2k  12156  lmcvg  12167  iscnp4  12168  cnima  12170  cnco  12171  cnclima  12173  cnntri  12174  cnntr  12175  cnss1  12176  cnss2  12177  cncnpi  12178  cncnp  12180  cnrest  12185  cnrest2  12186  cnrest2r  12187  lmss  12196  lmres  12198  lmcn  12201  txuni2  12206  txbasex  12207  eltx  12209  txtop  12210  txtopon  12212  txopn  12215  txss12  12216  txbasval  12217  neitx  12218  txcnp  12221  upxp  12222  txcnmpt  12223  uptx  12224  txcn  12225  txrest  12226  txdis1cn  12228  txlm  12229  lmcn2  12230  cnmpt11  12233  cnmpt11f  12234  cnmpt1t  12235  cnmpt12  12237  cnmpt21  12241  cnmpt21f  12242  cnmpt2t  12243  cnmpt22  12244  cnmpt1res  12246  cnmpt2res  12247  cnmptcom  12248  imasnopn  12249  xmet0  12291  blfvalps  12313  blfps  12337  blf  12338  blpnfctr  12367  xmetresbl  12368  isxms2  12380  xmstps  12385  msxms  12386  xmsxmet  12388  msmet  12389  xmspropd  12405  mspropd  12406  neibl  12419  bdxmet  12429  bdmopn  12432  mopnex  12433  metcnpd  12442  cnmet  12452  remetdval  12458  resubmet  12467  tgioo2cntop  12468  divccncfap  12490  cncfmet  12492  cncfcncntop  12493  cncfmptc  12495  cncfmptid  12496  cncfmpt1f  12497  cdivcncfap  12499  negfcncf  12501  mulcncflem  12502  mulcncf  12503  limcimolemlt  12513  cnplimcim  12516  cnlimcim  12517  cnmptlimc  12519  limccnpcntop  12520  reldvg  12521  dvfvalap  12523  dvcl  12525  dvbss  12527  dvfgg  12530  dvidlemap  12533  ex-or  12537  ex-an  12538  1kp2ke3k  12539  ex-exp  12542  ex-fac  12543  bj-2inf  12721  bj-inf2vnlem1  12753  nnsf  12783  peano3nninf  12785  nninfalllemn  12786  nninfself  12793  nninfsellemeqinf  12796  nninffeq  12800  trilpolemcl  12814  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818