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  6432  mulnnnq0  6433  genpprecll  6497  genppreclu  6498  addsrpr  6673  mulsrpr  6674  0nsr  6677  00sr  6697  opelreal  6726  eqresr  6733  axprecex  6764  ltxrlt  6882  pncan3  7016  apreim  7387  divcanap2  7441  divcanap3  7457  nn1gt1  7728  0nn0  7972  0z  8032  4t4e16  8216  5t4e20  8218  6t3e18  8221  6t4e24  8222  6t5e30  8223  7t3e21  8226  7t4e28  8227  7t5e35  8228  7t6e42  8229  7t7e49  8230  8t3e24  8232  8t4e32  8233  8t5e40  8234  8t7e56  8236  8t8e64  8237  9t3e27  8239  9t4e36  8240  9t5e45  8241  9t6e54  8242  9t7e63  8243  9t8e72  8244  9t9e81  8245  znq  8335  ltpnf  8472  mnflt  8474  mnfltpnf  8476  xnegpnf  8511  xnegmnf  8512  lincmb01cmp  8641  iccf1o  8642  elfzuz2  8663  fseq1m1p1  8727  fz0tp  8751  frecuzrdgrrn  8875  uzenom  8883  fzfig  8887  nnenom  8891  iseqeq1  8894  iseqeq4  8897  iseqval  8900  iseqfn  8901  iseq1  8902  iseqcl  8903  iseqp1  8904  exp0  8913  0exp  8944  sq0  8997  bj-2inf  9397  bj-inf2vnlem1  9430
  Copyright terms: Public domain W3C validator