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

Theorem eqid 2056
 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 164 . 2
21eqriv 2053 1
 Colors of variables: wff set class Syntax hints:   wceq 1259   wcel 1409 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-cleq 2049 This theorem is referenced by:  eqidd  2057  neirr  2229  sbsbc  2791  sbceqal  2841  dfnul2  3254  snidg  3428  prid1g  3502  tpid1  3509  tpid2  3510  tpid3  3512  dfiin2g  3718  syl5eqbr  3825  syl5eqbrr  3826  syl6breq  3831  opabbii  3852  mpteq2ia  3871  mpteq2da  3874  sucidg  4181  onsucelsucexmidlem1  4281  regexmidlemm  4285  regexmidlem1  4286  reg2exmidlema  4287  regexmid  4288  reg2exmid  4289  reg3exmid  4332  tfisi  4338  finds1  4353  nn0suc  4355  nndceq0  4367  0elnn  4368  nnregexmid  4370  opelxp  4402  relopab  4492  relop  4514  ididg  4517  elrnmpt1s  4612  dfiun3g  4617  dfiin3g  4618  dmmptg  4846  funfn  4959  mpt0  5054  f0  5108  dffn4  5140  f1orn  5164  f1oabexg  5166  f1o00  5189  f1o0  5191  fnbrfvb  5242  fnrnfv  5248  funfvdm  5264  fvmptg  5276  fvmptd  5281  fvmpt2d  5285  fvmptdf  5286  mpteqb  5289  fvmptt  5290  funfvop  5307  eldmrexrn  5336  fmpt2d  5355  fmptco  5358  fmptcof  5359  fnasrn  5369  fnasrng  5371  mptexg  5414  eufnfv  5417  idref  5424  f1elima  5440  fliftrel  5460  fliftel  5461  fliftel1  5462  fliftcnv  5463  fliftf  5467  riotabiia  5513  acexmidlem2  5537  acexmidlemv  5538  oprabbii  5588  mpt2eq12  5593  ovmpt2dxf  5654  ovmpt2df  5660  ov6g  5666  f1ocnvd  5730  f1opw2  5734  suppssfv  5736  suppssov1  5737  fnofval  5749  off  5752  offval2  5754  ofrfval2  5755  caofinvl  5761  abrexex  5772  abrexexg  5773  offres  5790  ofmres  5791  op1steq  5833  reldm  5840  mpt2exga  5863  mpt2ex  5864  fmpt2co  5865  cnvf1o  5874  f1od2  5884  tposssxp  5895  brtpos2  5897  tpos0  5920  iunon  5930  tfr2a  5967  tfrlemisucfn  5969  tfri1d  5980  tfrex  5985  tfrfun  5986  rdgfun  5991  rdg0  6005  frec0g  6014  frecfnom  6017  frecsuclem1  6018  frecsuclemdm  6019  frecsuclem3  6021  0lt1o  6054  oafnex  6055  omfnex  6060  fnoei  6063  oeiexg  6064  oeiv  6067  oacl  6071  omcl  6072  oeicl  6073  oav2  6074  omv2  6076  eqer  6169  ecelqsg  6190  elqsn0m  6205  qsel  6214  qliftf  6222  ecoptocl  6224  eroprf  6230  ecopovsym  6233  ecopovtrn  6234  ecopovsymg  6236  ecopovtrng  6237  th3qlem2  6240  th3q  6242  en2d  6279  en3d  6280  dom2lem  6283  dom2  6286  xpcomen  6332  fidifsnen  6362  supsnti  6409  0npi  6469  indpi  6498  recidnq  6549  addnnnq0  6605  mulnnnq0  6606  genpprecll  6670  genppreclu  6671  caucvgprpr  6868  addsrpr  6888  mulsrpr  6889  0nsr  6892  00sr  6912  caucvgsrlemgt1  6937  opelreal  6962  eqresr  6970  axprecex  7012  nntopi  7026  ltxrlt  7144  pncan3  7282  apreim  7668  divcanap2  7733  divcanap3  7749  nn1gt1  8023  0nn0  8254  0z  8313  decaddm10  8485  decmulnc  8493  10p10e20  8521  4t4e16  8525  5t4e20  8528  6t3e18  8531  6t4e24  8532  6t5e30  8533  7t3e21  8536  7t4e28  8537  7t5e35  8538  7t6e42  8539  7t7e49  8540  8t3e24  8542  8t4e32  8543  8t5e40  8544  8t7e56  8546  8t8e64  8547  9t3e27  8549  9t4e36  8550  9t5e45  8551  9t6e54  8552  9t7e63  8553  9t8e72  8554  9t9e81  8555  znq  8656  ltpnf  8803  mnflt  8805  mnfltpnf  8807  xnegpnf  8842  xnegmnf  8843  lincmb01cmp  8972  iccf1o  8973  elfzuz2  8995  fseq1m1p1  9059  fz0tp  9083  flqdiv  9271  frecuzrdgrrn  9358  uzenom  9366  fzfig  9370  nnenom  9374  iseqeq1  9378  iseqeq4  9381  iseqval  9384  iseqfn  9385  iseq1  9386  iseqcl  9387  iseqp1  9389  monoord2  9400  iseqdistr  9414  serile  9418  exp0  9424  0exp  9455  sq0  9510  sq10  9584  sq10e99m1  9585  shftfibg  9649  shftfib  9652  shftfn  9653  2shfti  9660  cvg1n  9813  resqrexlemsqa  9851  climconst2  10043  climres  10055  climshft  10056  iserclim0  10057  climle  10085  clim2iser  10088  clim2iser2  10089  climub  10095  climcvg1n  10100  climcaucn  10101  serif0  10102  dvdsmul2  10130  odd2np1lem  10183  ex-or  10276  ex-an  10277  1kp2ke3k  10278  ex-fac  10281  bj-2inf  10449  bj-inf2vnlem1  10482
 Copyright terms: Public domain W3C validator