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

Theorem eqid 2040
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 2037 1 𝐴 = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1243  wcel 1393
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 1338  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  eqidd  2041  neirr  2213  sbsbc  2765  sbceqal  2811  dfnul2  3223  snidg  3397  prid1g  3471  tpid1  3478  tpid2  3479  tpid3  3481  dfiin2g  3687  syl5eqbr  3794  syl5eqbrr  3795  syl6breq  3800  opabbii  3821  mpteq2ia  3840  mpteq2da  3843  sucidg  4140  onsucelsucexmidlem1  4240  regexmidlemm  4244  regexmidlem1  4245  regexmid  4246  tfisi  4288  finds1  4303  nn0suc  4305  nndceq0  4317  0elnn  4318  nnregexmid  4320  opelxp  4352  relopab  4442  relop  4464  ididg  4467  elrnmpt1s  4562  dfiun3g  4567  dfiin3g  4568  dmmptg  4796  funfn  4909  mpt0  5004  f0  5058  dffn4  5090  f1orn  5114  f1oabexg  5116  f1o00  5139  f1o0  5141  fnbrfvb  5192  fnrnfv  5198  funfvdm  5214  fvmptg  5226  fvmptd  5231  fvmpt2d  5235  fvmptdf  5236  mpteqb  5239  fvmptt  5240  funfvop  5257  eldmrexrn  5286  fmpt2d  5305  fmptco  5308  fmptcof  5309  fnasrn  5319  fnasrng  5321  mptexg  5364  eufnfv  5367  idref  5374  f1elima  5390  fliftrel  5410  fliftel  5411  fliftel1  5412  fliftcnv  5413  fliftf  5417  riotabiia  5463  acexmidlem2  5487  acexmidlemv  5488  oprabbii  5538  mpt2eq12  5543  ovmpt2dxf  5604  ovmpt2df  5610  ov6g  5616  f1ocnvd  5680  f1opw2  5684  suppssfv  5686  suppssov1  5687  fnofval  5699  off  5702  offval2  5704  ofrfval2  5705  caofinvl  5711  abrexex  5722  abrexexg  5723  offres  5740  ofmres  5741  op1steq  5783  reldm  5790  mpt2exga  5813  mpt2ex  5814  fmpt2co  5815  cnvf1o  5824  tposssxp  5842  brtpos2  5844  tpos0  5867  iunon  5877  tfr2a  5914  tfrlemisucfn  5916  tfri1d  5927  tfrex  5932  tfrfun  5933  rdgfun  5938  rdg0  5952  frec0g  5961  frecfnom  5964  frecsuclem1  5965  frecsuclemdm  5966  frecsuclem3  5968  0lt1o  6001  oafnex  6002  omfnex  6007  fnoei  6010  oeiexg  6011  oeiv  6014  oacl  6018  omcl  6019  oeicl  6020  oav2  6021  omv2  6023  eqer  6116  ecelqsg  6137  elqsn0m  6152  qsel  6161  qliftf  6169  ecoptocl  6171  eroprf  6177  ecopovsym  6180  ecopovtrn  6181  ecopovsymg  6183  ecopovtrng  6184  th3qlem2  6187  th3q  6189  en2d  6226  en3d  6227  dom2lem  6230  dom2  6233  xpcomen  6279  fidifsnen  6309  0npi  6383  indpi  6412  recidnq  6463  addnnnq0  6519  mulnnnq0  6520  genpprecll  6584  genppreclu  6585  caucvgprpr  6782  addsrpr  6802  mulsrpr  6803  0nsr  6806  00sr  6826  caucvgsrlemgt1  6851  opelreal  6876  eqresr  6884  axprecex  6926  nntopi  6940  ltxrlt  7056  pncan3  7190  apreim  7561  divcanap2  7626  divcanap3  7642  nn1gt1  7914  0nn0  8159  0z  8219  4t4e16  8403  5t4e20  8405  6t3e18  8408  6t4e24  8409  6t5e30  8410  7t3e21  8413  7t4e28  8414  7t5e35  8415  7t6e42  8416  7t7e49  8417  8t3e24  8419  8t4e32  8420  8t5e40  8421  8t7e56  8423  8t8e64  8424  9t3e27  8426  9t4e36  8427  9t5e45  8428  9t6e54  8429  9t7e63  8430  9t8e72  8431  9t9e81  8432  znq  8522  ltpnf  8660  mnflt  8662  mnfltpnf  8664  xnegpnf  8699  xnegmnf  8700  lincmb01cmp  8829  iccf1o  8830  elfzuz2  8851  fseq1m1p1  8915  fz0tp  8939  frecuzrdgrrn  9063  uzenom  9071  fzfig  9075  nnenom  9079  iseqeq1  9083  iseqeq4  9086  iseqval  9089  iseqfn  9090  iseq1  9091  iseqcl  9092  iseqp1  9094  monoord2  9105  iseqdistr  9118  serile  9122  exp0  9128  0exp  9159  sq0  9213  shftfibg  9290  shftfib  9293  shftfn  9294  2shfti  9301  cvg1n  9454  resqrexlemsqa  9491  climconst2  9680  climres  9692  climshft  9693  iserclim0  9694  climle  9722  clim2iser  9725  clim2iser2  9726  climub  9732  climcvg1n  9737  climcaucn  9738  serif0  9739  bj-2inf  9926  bj-inf2vnlem1  9959
  Copyright terms: Public domain W3C validator