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  0npi  7121  indpi  7150  recidnq  7201  addnnnq0  7257  mulnnnq0  7258  genpprecll  7322  genppreclu  7323  caucvgprpr  7520  addsrpr  7553  mulsrpr  7554  0nsr  7557  00sr  7577  caucvgsrlemgt1  7603  opelreal  7635  eqresr  7644  axprecex  7688  nntopi  7702  axpre-suploc  7710  ltxrlt  7830  pncan3  7970  apreim  8365  divcanap2  8440  divcanap3  8458  lble  8705  sup3exmid  8715  nn1gt1  8754  0nn0  8992  pnf0xnn0  9047  0z  9065  decaddm10  9240  decmulnc  9248  10p10e20  9276  4t4e16  9280  5t4e20  9283  6t3e18  9286  6t4e24  9287  6t5e30  9288  7t3e21  9291  7t4e28  9292  7t5e35  9293  7t6e42  9294  7t7e49  9295  8t3e24  9297  8t4e32  9298  8t5e40  9299  8t7e56  9301  8t8e64  9302  9t3e27  9304  9t4e36  9305  9t5e45  9306  9t6e54  9307  9t7e63  9308  9t8e72  9309  9t9e81  9310  infrenegsupex  9389  znq  9416  ltpnf  9567  mnflt  9569  mnfltpnf  9571  xnegpnf  9611  xnegmnf  9612  xaddpnf1  9629  xaddpnf2  9630  xaddmnf1  9631  xaddmnf2  9632  pnfaddmnf  9633  mnfaddpnf  9634  lincmb01cmp  9786  iccf1o  9787  elfzuz2  9809  fseq1m1p1  9875  fz0tp  9901  flqdiv  10094  frec2uzzd  10173  frec2uzsucd  10174  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgsuctlem  10196  uzenom  10198  fzfig  10203  nnenom  10207  seqeq1  10221  seq3val  10231  seqvalcd  10232  seqf  10234  seq3p1  10235  seqovcd  10236  seqp1cd  10239  seq3feq2  10243  seq3feq  10245  monoord2  10250  ser3mono  10251  seq3split  10252  seq3caopr2  10255  iseqf1olemqk  10267  seq3f1olemqsumkj  10271  seq3f1olemstep  10274  seq3f1oleml  10276  seq3f1o  10277  seq3homo  10283  seq3z  10284  seqfeq3  10285  seq3distr  10286  ser0f  10288  ser3ge0  10290  ser3le  10291  exp0  10297  0exp  10328  sq0  10383  sq10  10459  sq10e99m1  10460  facnn  10473  fac0  10474  bcval5  10509  hashinfom  10524  hashennn  10526  hashcl  10527  hashfz1  10529  hashen  10530  hash0  10543  fihashdom  10549  hashun  10551  seq3coll  10585  shftfibg  10592  shftfib  10595  shftfn  10596  2shfti  10603  seq3shft  10610  cvg1n  10758  resqrexlemsqa  10796  negfi  10999  xrmaxiflemcom  11018  xrmaxif  11020  infxrnegsupex  11032  climconst2  11060  climres  11072  climshft  11073  serclim0  11074  climle  11103  clim2ser  11106  clim2ser2  11107  climub  11113  climcvg1n  11119  climcaucn  11120  serf0  11121  sumfct  11143  fsum3cvg  11147  summodclem2  11151  zsumdc  11153  fsum3  11156  isumz  11158  fsumf1o  11159  isumss  11160  fsum3cvg2  11163  fsumsersdc  11164  fsum3ser  11166  fsumcl2lem  11167  fsumadd  11175  fsumsplitf  11177  sumsnf  11178  isummulc2  11195  isumadd  11200  fsumcnv  11206  mptfzshft  11211  fsumrev  11212  fsumshft  11213  fsummulc2  11217  iserabs  11244  isumshft  11259  isum1p  11261  isumlessdc  11265  divcnv  11266  trireciplem  11269  trirecip  11270  expcnvap0  11271  expcnvre  11272  expcnv  11273  explecnv  11274  geolim  11280  geolim2  11281  geo2lim  11285  geoisum  11286  geoisumr  11287  geoisum1  11288  geoisum1c  11289  cvgratnnlemseq  11295  cvgratz  11301  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  clim2prod  11308  clim2divap  11309  prodfap0  11314  prodfrecap  11315  prodfdivap  11316  prodeq2w  11325  fproddccvg  11341  prodmodclem2  11346  efcllemp  11364  efval  11367  eff  11369  efcvgfsum  11373  reefcl  11374  ege2le3  11377  ef0  11378  efcj  11379  efaddlem  11380  efadd  11381  eftlcl  11394  reeftlcl  11395  eftlub  11396  efsep  11397  effsumlt  11398  efgt1p2  11401  efgt1p  11402  eflegeo  11408  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  eirraplem  11483  eirrap  11484  egt2lt3  11486  dvdsmul2  11516  odd2np1lem  11569  gcd0val  11649  gcd0id  11667  bezoutlemnewy  11684  eucalgcvga  11739  eucalg  11740  lcm0val  11746  qnumdencoprm  11871  qeqnumdivden  11872  phimul  11902  hashgcdeq  11904  xpnnen  11907  ennnfonelemk  11913  ennnfonelemj0  11914  ennnfonelem0  11918  ennnfonelemnn0  11935  ctinfom  11941  ctiunct  11953  ressid  12020  2strstr1g  12062  srngstrd  12081  ipsstrd  12100  elrest  12127  elrestr  12128  topnpropgd  12134  toptopon2  12186  toponmax  12192  tpstop  12202  tpspropd  12203  tsettps  12205  eltpsg  12207  tgiun  12242  ntrval  12279  clsval  12280  0cld  12281  uncld  12282  cldcls  12283  ntr0  12303  isopn3i  12304  neif  12310  neival  12312  neii2  12318  neiss  12319  opnneiss  12327  innei  12332  neissex  12334  tgrest  12338  stoig  12342  restco  12343  resttopon2  12347  restopn2  12352  cnpval  12367  cntop1  12370  cntop2  12371  cnprcl2k  12375  lmcvg  12386  iscnp4  12387  cnima  12389  cnco  12390  cnclima  12392  cnntri  12393  cnntr  12394  cnss1  12395  cnss2  12396  cncnpi  12397  cncnp  12399  cnrest  12404  cnrest2  12405  cnrest2r  12406  lmss  12415  lmres  12417  lmcn  12420  txuni2  12425  txbasex  12426  eltx  12428  txtop  12429  txtopon  12431  txopn  12434  txss12  12435  txbasval  12436  neitx  12437  txcnp  12440  upxp  12441  txcnmpt  12442  uptx  12443  txcn  12444  txrest  12445  txdis1cn  12447  txlm  12448  lmcn2  12449  cnmpt11  12452  cnmpt11f  12453  cnmpt1t  12454  cnmpt12  12456  cnmpt21  12460  cnmpt21f  12461  cnmpt2t  12462  cnmpt22  12463  cnmpt1res  12465  cnmpt2res  12466  cnmptcom  12467  imasnopn  12468  hmeocnv  12476  hmeoopn  12480  hmeocld  12481  hmeontr  12482  hmeoimaf1o  12483  hmeores  12484  txhmeo  12488  txswaphmeo  12490  xmet0  12532  blfvalps  12554  blfps  12578  blf  12579  blpnfctr  12608  xmetresbl  12609  isxms2  12621  xmstps  12626  msxms  12627  xmsxmet  12629  msmet  12630  xmspropd  12646  mspropd  12647  neibl  12660  bdxmet  12670  bdmopn  12673  mopnex  12674  xmetxp  12676  xmettxlem  12678  xmettx  12679  txmetcnp  12687  metcnpd  12689  cnmet  12699  unicntopcntop  12705  cnopncntop  12706  remetdval  12708  resubmet  12717  tgioo2cntop  12718  addcncntoplem  12720  divcnap  12724  fsumcncntop  12725  divccncfap  12746  cncfmet  12748  cncfcncntop  12749  cncfmptc  12751  cncfmptid  12752  cncfmpt1f  12753  cncfmpt2fcntop  12754  cdivcncfap  12756  negfcncf  12758  mulcncflem  12759  mulcncf  12760  cnopnap  12763  ivthinc  12790  ivthdec  12791  limcmpted  12801  limcimolemlt  12802  cnplimcim  12805  cnplimclemr  12807  cnlimcim  12809  cnlimc  12810  cnmptlimc  12812  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  reldvg  12817  dvfvalap  12819  dvcl  12821  dvbss  12823  dvfgg  12826  dvidlemap  12829  dvcnp2cntop  12832  dvcn  12833  dvaddxxbr  12834  dvmulxxbr  12835  dvaddxx  12836  dvmulxx  12837  dviaddf  12838  dvimulf  12839  dvcoapbr  12840  dvcjbr  12841  dvrecap  12846  dveflem  12855  dvef  12856  sincn  12858  coscn  12859  ex-or  12934  ex-an  12935  1kp2ke3k  12936  ex-exp  12939  ex-fac  12940  bj-2inf  13136  bj-inf2vnlem1  13168  subctctexmid  13196  nnsf  13199  peano3nninf  13201  nninfalllemn  13202  nninfself  13209  nninfsellemeqinf  13212  nninffeq  13216  trilpolemcl  13230  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234