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

Theorem eqid 2018
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 A = A

Proof of Theorem eqid
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 biid 160 . 2 (x Ax A)
21eqriv 2015 1 A = A
Colors of variables: wff set class
Syntax hints:   = wceq 1226   wcel 1370
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 1314  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-cleq 2011
This theorem is referenced by:  eqidd  2019  neirr  2190  sbsbc  2741  sbceqal  2787  dfnul2  3199  snidg  3371  prid1g  3444  tpid1  3451  tpid2  3452  tpid3  3454  dfiin2g  3660  syl5eqbr  3767  syl5eqbrr  3768  syl6breq  3773  opabbii  3794  mpteq2ia  3813  mpteq2da  3816  sucidg  4098  onsucelsucexmidlem1  4193  regexmidlemm  4197  regexmidlem1  4198  regexmid  4199  tfisi  4233  finds1  4248  nn0suc  4250  nndceq0  4262  0elnn  4263  nnregexmid  4265  opelxp  4297  relopab  4387  relop  4409  ididg  4412  elrnmpt1s  4507  dfiun3g  4512  dfiin3g  4513  dmmptg  4741  funfn  4853  mpt0  4948  f0  5001  dffn4  5033  f1orn  5057  f1oabexg  5059  f1o00  5082  f1o0  5084  fnbrfvb  5135  fnrnfv  5141  funfvdm  5157  fvmptg  5169  fvmptd  5174  fvmpt2d  5178  fvmptdf  5179  mpteqb  5182  fvmptt  5183  funfvop  5200  eldmrexrn  5229  fmpt2d  5248  fmptco  5251  fmptcof  5252  fnasrn  5262  fnasrng  5264  mptexg  5307  eufnfv  5310  idref  5317  f1elima  5333  fliftrel  5353  fliftel  5354  fliftel1  5355  fliftcnv  5356  fliftf  5360  riotabiia  5405  acexmidlem2  5429  acexmidlemv  5430  oprabbii  5479  mpt2eq12  5484  ovmpt2dxf  5545  ovmpt2df  5551  ov6g  5557  f1ocnvd  5621  f1opw2  5625  suppssfv  5627  suppssov1  5628  fnofval  5640  off  5643  offval2  5645  ofrfval2  5646  caofinvl  5652  abrexex  5663  abrexexg  5664  offres  5681  ofmres  5682  op1steq  5724  reldm  5731  mpt2exga  5754  mpt2ex  5755  fmpt2co  5756  cnvf1o  5765  tposssxp  5782  brtpos2  5784  tpos0  5807  iunon  5817  tfr2a  5854  tfrlemisucfn  5855  tfri1d  5867  tfri1  5869  tfrex  5872  rdgfun  5877  rdgi0g  5882  rdg0  5891  frecfnom  5897  frec0g  5898  frecsuclem1  5899  frecsuclemdm  5900  frecsuclem3  5902  0lt1o  5934  oafnex  5935  omfnex  5940  fnoei  5943  oeiexg  5944  oeiv  5947  oa0  5948  oei0  5950  oacl  5951  omcl  5952  oeicl  5953  oav2  5954  omv2  5956  eqer  6045  ecelqsg  6066  elqsn0m  6081  qsel  6090  qliftf  6098  ecoptocl  6100  eroprf  6106  ecopovsym  6109  ecopovtrn  6110  ecopovsymg  6112  ecopovtrng  6113  th3qlem2  6116  th3q  6118  0npi  6167  recidnq  6246  addnnnq0  6298  mulnnnq0  6299  genpprecll  6362  genppreclu  6363  addsrpr  6486  mulsrpr  6487  0nsr  6490  00sr  6510  opelreal  6534  eqresr  6541  axprecex  6568  ltxrlt  6680  pncan3  6806  bj-2inf  7299  bj-inf2vnlem1  7327
  Copyright terms: Public domain W3C validator