ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqid GIF version

Theorem eqid 2082
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.
StepHypRef Expression
1 biid 169 . 2 (𝑥𝐴𝑥𝐴)
21eqriv 2079 1 𝐴 = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1285  wcel 1434
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 1379  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  eqidd  2083  neirr  2255  sbsbc  2820  sbceqal  2870  dfnul2  3260  snidg  3431  prid1g  3504  tpid1  3511  tpid2  3512  tpid3  3514  dfiin2g  3719  syl5eqbr  3826  syl5eqbrr  3827  syl6breq  3832  opabbii  3853  mpteq2ia  3872  mpteq2da  3875  sucidg  4179  onsucelsucexmidlem1  4279  regexmidlemm  4283  regexmidlem1  4284  reg2exmidlema  4285  regexmid  4286  reg2exmid  4287  reg3exmid  4330  tfisi  4336  finds1  4351  nn0suc  4353  nndceq0  4365  0elnn  4366  nnregexmid  4368  opelxp  4400  relopab  4492  relop  4514  ididg  4517  elrnmpt1s  4612  dfiun3g  4617  dfiin3g  4618  dmmptg  4848  funfn  4961  mpt0  5057  f0  5111  dffn4  5143  f1orn  5167  f1oabexg  5169  f1o00  5192  f1o0  5194  fnbrfvb  5246  fnrnfv  5252  funfvdm  5268  fvmptg  5280  fvmptd  5285  fvmpt2d  5289  fvmptdf  5290  mpteqb  5293  fvmptt  5294  funfvop  5311  eldmrexrn  5340  fmpt2d  5359  fmptco  5362  fmptcof  5363  fnasrn  5373  fnasrng  5375  mptexg  5418  eufnfv  5421  idref  5428  f1elima  5444  fliftrel  5463  fliftel  5464  fliftel1  5465  fliftcnv  5466  fliftf  5470  riotabiia  5516  acexmidlem2  5540  acexmidlemv  5541  oprabbii  5591  mpt2eq12  5596  ovmpt2dxf  5657  ovmpt2df  5663  ov6g  5669  f1ocnvd  5733  f1opw2  5737  suppssfv  5739  suppssov1  5740  fnofval  5752  off  5755  offval2  5757  ofrfval2  5758  caofinvl  5764  abrexex  5775  abrexexg  5776  offres  5793  ofmres  5794  op1steq  5836  reldm  5843  mpt2exga  5866  mpt2ex  5867  fmpt2co  5868  cnvf1o  5877  f1od2  5887  tposssxp  5898  brtpos2  5900  tpos0  5923  iunon  5933  tfrfun  5969  tfr2a  5970  tfrlemisucfn  5973  tfri1d  5984  tfr1onlemsucfn  5989  tfr1onlemubacc  5995  tfr1on  5999  tfri1dALT  6000  tfrcllemubacc  6008  tfrex  6017  rdgfun  6022  rdgon  6035  rdg0  6036  frec0g  6046  frecfnom  6050  freccllem  6051  freccl  6052  frecfcllem  6053  frecfcl  6054  frecsuclem  6055  0lt1o  6087  oafnex  6088  omfnex  6093  fnoei  6096  oeiexg  6097  oeiv  6100  oacl  6104  omcl  6105  oeicl  6106  oav2  6107  omv2  6109  eqer  6204  ecelqsg  6225  elqsn0m  6240  qsel  6249  qliftf  6257  ecoptocl  6259  eroprf  6265  ecopovsym  6268  ecopovtrn  6269  ecopovsymg  6271  ecopovtrng  6272  th3qlem2  6275  th3q  6277  en2d  6315  en3d  6316  dom2lem  6319  dom2  6322  1domsn  6363  xpcomen  6371  xpf1o  6385  fidifsnen  6405  supsnti  6477  0npi  6565  indpi  6594  recidnq  6645  addnnnq0  6701  mulnnnq0  6702  genpprecll  6766  genppreclu  6767  caucvgprpr  6964  addsrpr  6984  mulsrpr  6985  0nsr  6988  00sr  7008  caucvgsrlemgt1  7033  opelreal  7058  eqresr  7066  axprecex  7108  nntopi  7122  ltxrlt  7245  pncan3  7383  apreim  7770  divcanap2  7835  divcanap3  7853  lble  8092  nn1gt1  8139  0nn0  8370  pnf0xnn0  8425  0z  8443  decaddm10  8616  decmulnc  8624  10p10e20  8652  4t4e16  8656  5t4e20  8659  6t3e18  8662  6t4e24  8663  6t5e30  8664  7t3e21  8667  7t4e28  8668  7t5e35  8669  7t6e42  8670  7t7e49  8671  8t3e24  8673  8t4e32  8674  8t5e40  8675  8t7e56  8677  8t8e64  8678  9t3e27  8680  9t4e36  8681  9t5e45  8682  9t6e54  8683  9t7e63  8684  9t8e72  8685  9t9e81  8686  infrenegsupex  8763  znq  8790  ltpnf  8932  mnflt  8934  mnfltpnf  8936  xnegpnf  8971  xnegmnf  8972  lincmb01cmp  9101  iccf1o  9102  elfzuz2  9124  fseq1m1p1  9188  fz0tp  9212  flqdiv  9403  frec2uzzd  9482  frec2uzsucd  9483  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgsuctlem  9505  uzenom  9507  fzfig  9512  nnenom  9516  iseqeq1  9524  iseqeq4  9527  iseqval  9530  iseqvalt  9532  iseq1  9533  iseqfcl  9535  iseqfclt  9536  iseqcl  9537  iseqp1  9538  iseqp1t  9539  iseqoveq  9540  iseqss  9541  iseqsst  9542  iseqfeq2  9545  iseqfeq  9547  monoord2  9552  iseqdistr  9567  iser0f  9569  serile  9571  exp0  9577  0exp  9608  sq0  9663  sq10  9737  sq10e99m1  9738  facnn  9751  fac0  9752  sizeinf  9802  sizeennn  9804  sizecl  9805  sizefz1  9807  sizeen  9808  size0  9821  sizedom  9827  sizeun  9829  shftfibg  9846  shftfib  9849  shftfn  9850  2shfti  9857  cvg1n  10010  resqrexlemsqa  10048  negfi  10248  climconst2  10268  climres  10280  climshft  10281  iserclim0  10282  climle  10310  clim2iser  10313  clim2iser2  10314  climub  10320  climcvg1n  10325  climcaucn  10326  serif0  10327  fisumcvg  10338  dvdsmul2  10363  odd2np1lem  10416  gcd0val  10496  gcd0id  10514  bezoutlemnewy  10529  eucialgcvga  10584  eucialg  10585  lcm0val  10591  xpnnen  10705  ex-or  10711  ex-an  10712  1kp2ke3k  10713  ex-fac  10716  bj-2inf  10891  bj-inf2vnlem1  10923
  Copyright terms: Public domain W3C validator