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

Theorem eqid 2085
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 2082 1 𝐴 = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1287  wcel 1436
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 1381  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqidd  2086  neirr  2260  sbsbc  2833  sbceqal  2883  dfnul2  3277  snidg  3455  prid1g  3528  tpid1  3535  tpid2  3536  tpid3  3538  dfiin2g  3745  syl5eqbr  3852  syl5eqbrr  3853  syl6breq  3858  opabbii  3879  mpteq2ia  3898  mpteq2da  3901  sucidg  4215  onsucelsucexmidlem1  4315  regexmidlemm  4319  regexmidlem1  4320  reg2exmidlema  4321  regexmid  4322  reg2exmid  4323  reg3exmid  4366  tfisi  4373  finds1  4388  nn0suc  4390  nndceq0  4402  0elnn  4403  nnregexmid  4405  opelxp  4438  relopab  4530  relop  4552  ididg  4555  elrnmpt1s  4651  dfiun3g  4656  dfiin3g  4657  dmmptg  4890  funfn  5006  mpt0  5102  f0  5157  dffn4  5195  f1orn  5219  f1oabexg  5221  f1o00  5244  f1o0  5246  fnbrfvb  5301  fnrnfv  5307  funfvdm  5323  fvmptg  5336  fvmptd  5341  fvmpt2d  5345  fvmptdf  5346  mpteqb  5349  fvmptt  5350  funfvop  5367  eldmrexrn  5396  fmpttd  5409  fmpt2d  5416  fmptco  5420  fmptcof  5421  fnasrn  5431  fnasrng  5433  mptexg  5476  eufnfv  5479  idref  5490  f1elima  5506  fliftrel  5525  fliftel  5526  fliftel1  5527  fliftcnv  5528  fliftf  5532  riotabiia  5579  acexmidlem2  5603  acexmidlemv  5604  oprabbii  5654  mpt2eq12  5659  ovmpt2dxf  5720  ovmpt2df  5726  ov6g  5732  f1ocnvd  5796  f1opw2  5800  suppssfv  5802  suppssov1  5803  fnofval  5815  off  5818  offval2  5820  ofrfval2  5821  caofinvl  5827  abrexex  5838  abrexexg  5839  offres  5856  ofmres  5857  op1steq  5899  reldm  5906  mpt2exga  5929  mpt2ex  5930  fmpt2co  5931  cnvf1o  5940  f1od2  5950  tposssxp  5961  brtpos2  5963  tpos0  5986  iunon  5996  tfrfun  6032  tfr2a  6033  tfrlemisucfn  6036  tfri1d  6047  tfr1onlemsucfn  6052  tfr1onlemubacc  6058  tfr1on  6062  tfri1dALT  6063  tfrcllemubacc  6071  tfrex  6080  rdgfun  6085  rdgon  6098  rdg0  6099  frec0g  6109  frecfnom  6113  freccllem  6114  freccl  6115  frecfcllem  6116  frecfcl  6117  frecsuclem  6118  0lt1o  6151  oafnex  6152  omfnex  6157  fnoei  6160  oeiexg  6161  oeiv  6164  oacl  6168  omcl  6169  oeicl  6170  oav2  6171  omv2  6173  eqer  6269  ecelqsg  6290  elqsn0m  6305  qsel  6314  qliftf  6322  ecoptocl  6324  eroprf  6330  ecopovsym  6333  ecopovtrn  6334  ecopovsymg  6336  ecopovtrng  6337  th3qlem2  6340  th3q  6342  mapsncnv  6397  mapsnf1o3  6399  en2d  6430  en3d  6431  dom2lem  6434  dom2  6437  1domsn  6480  xpcomen  6488  xpf1o  6505  mapxpen  6509  fidifsnen  6531  isbth  6612  supsnti  6636  djueq1  6669  djueq2  6670  djuf1olem  6681  updjud  6709  nnnninf  6742  0npi  6808  indpi  6837  recidnq  6888  addnnnq0  6944  mulnnnq0  6945  genpprecll  7009  genppreclu  7010  caucvgprpr  7207  addsrpr  7227  mulsrpr  7228  0nsr  7231  00sr  7251  caucvgsrlemgt1  7276  opelreal  7301  eqresr  7309  axprecex  7351  nntopi  7365  ltxrlt  7488  pncan3  7626  apreim  8013  divcanap2  8078  divcanap3  8096  lble  8335  nn1gt1  8382  0nn0  8613  pnf0xnn0  8668  0z  8686  decaddm10  8859  decmulnc  8867  10p10e20  8895  4t4e16  8899  5t4e20  8902  6t3e18  8905  6t4e24  8906  6t5e30  8907  7t3e21  8910  7t4e28  8911  7t5e35  8912  7t6e42  8913  7t7e49  8914  8t3e24  8916  8t4e32  8917  8t5e40  8918  8t7e56  8920  8t8e64  8921  9t3e27  8923  9t4e36  8924  9t5e45  8925  9t6e54  8926  9t7e63  8927  9t8e72  8928  9t9e81  8929  infrenegsupex  9006  znq  9033  ltpnf  9175  mnflt  9177  mnfltpnf  9179  xnegpnf  9214  xnegmnf  9215  lincmb01cmp  9344  iccf1o  9345  elfzuz2  9367  fseq1m1p1  9431  fz0tp  9455  flqdiv  9648  frec2uzzd  9727  frec2uzsucd  9728  frecuzrdgrrn  9735  frec2uzrdg  9736  frecuzrdgrcl  9737  frecuzrdgsuc  9741  frecuzrdgrclt  9742  frecuzrdgg  9743  frecuzrdgsuctlem  9750  uzenom  9752  fzfig  9757  nnenom  9761  iseqeq1  9774  iseqeq4  9777  iseqval  9780  iseqvalt  9782  iseq1  9783  iseqfcl  9785  iseqfclt  9786  iseqcl  9787  iseqp1  9788  iseqp1t  9789  iseqoveq  9790  iseqss  9791  iseqsst  9792  iseqfeq2  9795  iseqfeq  9797  monoord2  9802  iseqf1olemqk  9819  iseqf1olemstep  9826  iseqf1oleml  9828  iseqf1o  9829  iseqdistr  9838  iser0f  9840  serile  9843  exp0  9849  0exp  9880  sq0  9935  sq10  10009  sq10e99m1  10010  facnn  10023  fac0  10024  hashinfom  10074  hashennn  10076  hashcl  10077  hashfz1  10079  hashen  10080  hash0  10093  fihashdom  10099  hashun  10101  shftfibg  10142  shftfib  10145  shftfn  10146  2shfti  10153  cvg1n  10306  resqrexlemsqa  10344  negfi  10544  climconst2  10564  climres  10576  climshft  10577  iserclim0  10578  climle  10606  clim2iser  10609  clim2iser2  10610  climub  10616  climcvg1n  10621  climcaucn  10622  serif0  10623  sumfct  10645  fisumcvg  10648  isummolem2  10653  zisum  10655  fisum  10657  isumz  10659  fsumf1o  10660  isumss  10661  dvdsmul2  10685  odd2np1lem  10738  gcd0val  10818  gcd0id  10836  bezoutlemnewy  10851  eucialgcvga  10906  eucialg  10907  lcm0val  10913  qnumdencoprm  11037  qeqnumdivden  11038  phimul  11068  hashgcdeq  11070  xpnnen  11073  ex-or  11079  ex-an  11080  1kp2ke3k  11081  ex-fac  11084  bj-2inf  11262  bj-inf2vnlem1  11294  nnsf  11324  peano3nninf  11326  nninfalllemn  11327  nninfself  11334  nninfsellemeqinf  11337
  Copyright terms: Public domain W3C validator