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

Theorem eqid 2037
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 160 . 2
21eqriv 2034 1
Colors of variables: wff set class
Syntax hints:   wceq 1242   wcel 1390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1335  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  eqidd  2038  neirr  2210  sbsbc  2762  sbceqal  2808  dfnul2  3220  snidg  3392  prid1g  3465  tpid1  3472  tpid2  3473  tpid3  3475  dfiin2g  3681  syl5eqbr  3788  syl5eqbrr  3789  syl6breq  3794  opabbii  3815  mpteq2ia  3834  mpteq2da  3837  sucidg  4119  onsucelsucexmidlem1  4213  regexmidlemm  4217  regexmidlem1  4218  regexmid  4219  tfisi  4253  finds1  4268  nn0suc  4270  nndceq0  4282  0elnn  4283  nnregexmid  4285  opelxp  4317  relopab  4407  relop  4429  ididg  4432  elrnmpt1s  4527  dfiun3g  4532  dfiin3g  4533  dmmptg  4761  funfn  4874  mpt0  4969  f0  5023  dffn4  5055  f1orn  5079  f1oabexg  5081  f1o00  5104  f1o0  5106  fnbrfvb  5157  fnrnfv  5163  funfvdm  5179  fvmptg  5191  fvmptd  5196  fvmpt2d  5200  fvmptdf  5201  mpteqb  5204  fvmptt  5205  funfvop  5222  eldmrexrn  5251  fmpt2d  5270  fmptco  5273  fmptcof  5274  fnasrn  5284  fnasrng  5286  mptexg  5329  eufnfv  5332  idref  5339  f1elima  5355  fliftrel  5375  fliftel  5376  fliftel1  5377  fliftcnv  5378  fliftf  5382  riotabiia  5428  acexmidlem2  5452  acexmidlemv  5453  oprabbii  5502  mpt2eq12  5507  ovmpt2dxf  5568  ovmpt2df  5574  ov6g  5580  f1ocnvd  5644  f1opw2  5648  suppssfv  5650  suppssov1  5651  fnofval  5663  off  5666  offval2  5668  ofrfval2  5669  caofinvl  5675  abrexex  5686  abrexexg  5687  offres  5704  ofmres  5705  op1steq  5747  reldm  5754  mpt2exga  5777  mpt2ex  5778  fmpt2co  5779  cnvf1o  5788  tposssxp  5805  brtpos2  5807  tpos0  5830  iunon  5840  tfr2a  5877  tfrlemisucfn  5879  tfri1d  5890  tfrex  5895  rdgfun  5900  rdg0  5914  frec0g  5922  frecfnom  5925  frecsuclem1  5926  frecsuclemdm  5927  frecsuclem3  5929  0lt1o  5962  oafnex  5963  omfnex  5968  fnoei  5971  oeiexg  5972  oeiv  5975  oacl  5979  omcl  5980  oeicl  5981  oav2  5982  omv2  5984  eqer  6074  ecelqsg  6095  elqsn0m  6110  qsel  6119  qliftf  6127  ecoptocl  6129  eroprf  6135  ecopovsym  6138  ecopovtrn  6139  ecopovsymg  6141  ecopovtrng  6142  th3qlem2  6145  th3q  6147  en2d  6184  en3d  6185  dom2lem  6188  dom2  6191  xpcomen  6237  0npi  6297  indpi  6326  recidnq  6377  addnnnq0  6431  mulnnnq0  6432  genpprecll  6496  genppreclu  6497  addsrpr  6653  mulsrpr  6654  0nsr  6657  00sr  6677  opelreal  6706  eqresr  6713  axprecex  6744  ltxrlt  6862  pncan3  6996  apreim  7367  divcanap2  7421  divcanap3  7437  nn1gt1  7708  0nn0  7952  0z  8012  4t4e16  8196  5t4e20  8198  6t3e18  8201  6t4e24  8202  6t5e30  8203  7t3e21  8206  7t4e28  8207  7t5e35  8208  7t6e42  8209  7t7e49  8210  8t3e24  8212  8t4e32  8213  8t5e40  8214  8t7e56  8216  8t8e64  8217  9t3e27  8219  9t4e36  8220  9t5e45  8221  9t6e54  8222  9t7e63  8223  9t8e72  8224  9t9e81  8225  znq  8315  ltpnf  8452  mnflt  8454  mnfltpnf  8456  xnegpnf  8491  xnegmnf  8492  lincmb01cmp  8621  iccf1o  8622  elfzuz2  8643  fseq1m1p1  8707  fz0tp  8731  frecuzrdgrrn  8855  uzenom  8863  fzfig  8867  nnenom  8871  iseqeq1  8874  iseqeq4  8877  iseqval  8880  iseqfn  8881  iseq1  8882  iseqcl  8883  iseqp1  8884  exp0  8893  0exp  8924  sq0  8977  bj-2inf  9372  bj-inf2vnlem1  9400
  Copyright terms: Public domain W3C validator