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

Theorem eqid 2117
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 170 . 2  |-  ( x  e.  A  <->  x  e.  A )
21eqriv 2114 1  |-  A  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1316    e. wcel 1465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1410  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eqidd  2118  neirr  2294  sbsbc  2886  sbceqal  2936  dfnul2  3335  snidg  3524  prid1g  3597  tpid1  3604  tpid1g  3605  tpid2  3606  tpid2g  3607  tpid3  3609  dfiin2g  3816  eqbrtrid  3933  eqbrtrrid  3934  breqtrdi  3939  opabbii  3965  mpteq2ia  3984  mpteq2da  3987  sucidg  4308  onsucelsucexmidlem1  4413  regexmidlemm  4417  regexmidlem1  4418  reg2exmidlema  4419  regexmid  4420  reg2exmid  4421  reg3exmid  4464  tfisi  4471  finds1  4486  nn0suc  4488  nndceq0  4501  0elnn  4502  nnregexmid  4504  opelxp  4539  relopab  4636  relop  4659  ididg  4662  elrnmpt1s  4759  dfiun3g  4766  dfiin3g  4767  dmmptg  5006  funfn  5123  mpt0  5220  f0  5283  dffn4  5321  f1orn  5345  f1oabexg  5347  f1o00  5370  f1o0  5372  fnbrfvb  5430  fnrnfv  5436  funfvdm  5452  fvmptg  5465  fvmptd  5470  fvmpt2d  5475  fvmptdf  5476  mpteqb  5479  fvmptt  5480  funfvop  5500  eldmrexrn  5529  fvmptelrn  5541  fmpttd  5543  fmpt2d  5550  fmptco  5554  fmptcof  5555  fnasrn  5566  fnasrng  5568  mptexg  5613  eufnfv  5616  idref  5626  f1elima  5642  fliftrel  5661  fliftel  5662  fliftel1  5663  fliftcnv  5664  fliftf  5668  riotabiia  5715  acexmidlem2  5739  acexmidlemv  5740  oprabbii  5794  mpoeq12  5799  ovmpodxf  5864  ovmpodf  5870  ov6g  5876  f1ocnvd  5940  f1opw2  5944  suppssfv  5946  suppssov1  5947  ofvalg  5959  off  5962  offval2  5965  ofrfval2  5966  caofinvl  5972  abrexex  5983  abrexexg  5984  offres  6001  ofmres  6002  op1steq  6045  reldm  6052  mpoexga  6078  mpoex  6079  fnmpoovd  6080  fmpoco  6081  cnvf1o  6090  f1od2  6100  tposssxp  6114  brtpos2  6116  tpos0  6139  iunon  6149  tfrfun  6185  tfr2a  6186  tfrlemisucfn  6189  tfri1d  6200  tfr1onlemsucfn  6205  tfr1onlemubacc  6211  tfr1on  6215  tfri1dALT  6216  tfrcllemubacc  6224  tfrex  6233  rdgfun  6238  rdgon  6251  rdg0  6252  frec0g  6262  frecfnom  6266  freccllem  6267  freccl  6268  frecfcllem  6269  frecfcl  6270  frecsuclem  6271  0lt1o  6305  oafnex  6308  omfnex  6313  fnoei  6316  oeiexg  6317  oeiv  6320  oacl  6324  omcl  6325  oeicl  6326  oav2  6327  omv2  6329  eqer  6429  ecelqsg  6450  elqsn0m  6465  qsel  6474  qliftf  6482  ecoptocl  6484  eroprf  6490  ecopovsym  6493  ecopovtrn  6494  ecopovsymg  6496  ecopovtrng  6497  th3qlem2  6500  th3q  6502  mapsncnv  6557  mapsnf1o3  6559  mptelixpg  6596  ixpsnf1o  6598  en2d  6630  en3d  6631  dom2lem  6634  dom2  6637  1domsn  6681  xpcomen  6689  xpf1o  6706  mapxpen  6710  fidifsnen  6732  isbth  6823  elfir  6829  supsnti  6860  djueq1  6893  djueq2  6894  djuf1olem  6906  inl11  6918  updjud  6935  omp1eom  6948  difinfsn  6953  ctmlemr  6961  ctssdclemn0  6963  ctssdclemr  6965  ctssdc  6966  enumct  6968  nnnninf  6991  ismkvnex  6997  mkvprop  7000  exmidonfin  7018  exmidaclem  7032  exmidac  7033  0npi  7089  indpi  7118  recidnq  7169  addnnnq0  7225  mulnnnq0  7226  genpprecll  7290  genppreclu  7291  caucvgprpr  7488  addsrpr  7521  mulsrpr  7522  0nsr  7525  00sr  7545  caucvgsrlemgt1  7571  opelreal  7603  eqresr  7612  axprecex  7656  nntopi  7670  axpre-suploc  7678  ltxrlt  7798  pncan3  7938  apreim  8332  divcanap2  8407  divcanap3  8425  lble  8669  sup3exmid  8679  nn1gt1  8718  0nn0  8950  pnf0xnn0  9005  0z  9023  decaddm10  9198  decmulnc  9206  10p10e20  9234  4t4e16  9238  5t4e20  9241  6t3e18  9244  6t4e24  9245  6t5e30  9246  7t3e21  9249  7t4e28  9250  7t5e35  9251  7t6e42  9252  7t7e49  9253  8t3e24  9255  8t4e32  9256  8t5e40  9257  8t7e56  9259  8t8e64  9260  9t3e27  9262  9t4e36  9263  9t5e45  9264  9t6e54  9265  9t7e63  9266  9t8e72  9267  9t9e81  9268  infrenegsupex  9345  znq  9372  ltpnf  9522  mnflt  9524  mnfltpnf  9526  xnegpnf  9566  xnegmnf  9567  xaddpnf1  9584  xaddpnf2  9585  xaddmnf1  9586  xaddmnf2  9587  pnfaddmnf  9588  mnfaddpnf  9589  lincmb01cmp  9741  iccf1o  9742  elfzuz2  9764  fseq1m1p1  9830  fz0tp  9856  flqdiv  10049  frec2uzzd  10128  frec2uzsucd  10129  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgg  10144  frecuzrdgsuctlem  10151  uzenom  10153  fzfig  10158  nnenom  10162  seqeq1  10176  seq3val  10186  seqvalcd  10187  seqf  10189  seq3p1  10190  seqovcd  10191  seqp1cd  10194  seq3feq2  10198  seq3feq  10200  monoord2  10205  ser3mono  10206  seq3split  10207  seq3caopr2  10210  iseqf1olemqk  10222  seq3f1olemqsumkj  10226  seq3f1olemstep  10229  seq3f1oleml  10231  seq3f1o  10232  seq3homo  10238  seq3z  10239  seqfeq3  10240  seq3distr  10241  ser0f  10243  ser3ge0  10245  ser3le  10246  exp0  10252  0exp  10283  sq0  10338  sq10  10414  sq10e99m1  10415  facnn  10428  fac0  10429  bcval5  10464  hashinfom  10479  hashennn  10481  hashcl  10482  hashfz1  10484  hashen  10485  hash0  10498  fihashdom  10504  hashun  10506  seq3coll  10540  shftfibg  10547  shftfib  10550  shftfn  10551  2shfti  10558  seq3shft  10565  cvg1n  10713  resqrexlemsqa  10751  negfi  10954  xrmaxiflemcom  10973  xrmaxif  10975  infxrnegsupex  10987  climconst2  11015  climres  11027  climshft  11028  serclim0  11029  climle  11058  clim2ser  11061  clim2ser2  11062  climub  11068  climcvg1n  11074  climcaucn  11075  serf0  11076  sumfct  11098  fsum3cvg  11101  summodclem2  11106  zsumdc  11108  fsum3  11111  isumz  11113  fsumf1o  11114  isumss  11115  fsum3cvg2  11118  fsumsersdc  11119  fsum3ser  11121  fsumcl2lem  11122  fsumadd  11130  fsumsplitf  11132  sumsnf  11133  isummulc2  11150  isumadd  11155  fsumcnv  11161  mptfzshft  11166  fsumrev  11167  fsumshft  11168  fsummulc2  11172  iserabs  11199  isumshft  11214  isum1p  11216  isumlessdc  11220  divcnv  11221  trireciplem  11224  trirecip  11225  expcnvap0  11226  expcnvre  11227  expcnv  11228  explecnv  11229  geolim  11235  geolim2  11236  geo2lim  11240  geoisum  11241  geoisumr  11242  geoisum1  11243  geoisum1c  11244  cvgratnnlemseq  11250  cvgratz  11256  mertenslemub  11258  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  efcllemp  11278  efval  11281  eff  11283  efcvgfsum  11287  reefcl  11288  ege2le3  11291  ef0  11292  efcj  11293  efaddlem  11294  efadd  11295  eftlcl  11308  reeftlcl  11309  eftlub  11310  efsep  11311  effsumlt  11312  efgt1p2  11315  efgt1p  11316  eflegeo  11322  ef01bndlem  11377  sin01bnd  11378  cos01bnd  11379  eirraplem  11395  eirrap  11396  egt2lt3  11398  dvdsmul2  11428  odd2np1lem  11481  gcd0val  11561  gcd0id  11579  bezoutlemnewy  11596  eucalgcvga  11651  eucalg  11652  lcm0val  11658  qnumdencoprm  11782  qeqnumdivden  11783  phimul  11813  hashgcdeq  11815  xpnnen  11818  ennnfonelemk  11824  ennnfonelemj0  11825  ennnfonelem0  11829  ennnfonelemnn0  11846  ctinfom  11852  ctiunct  11864  ressid  11931  2strstr1g  11973  srngstrd  11992  ipsstrd  12011  elrest  12038  elrestr  12039  topnpropgd  12045  toptopon2  12097  toponmax  12103  tpstop  12113  tpspropd  12114  tsettps  12116  eltpsg  12118  tgiun  12153  ntrval  12190  clsval  12191  0cld  12192  uncld  12193  cldcls  12194  ntr0  12214  isopn3i  12215  neif  12221  neival  12223  neii2  12229  neiss  12230  opnneiss  12238  innei  12243  neissex  12245  tgrest  12249  stoig  12253  restco  12254  resttopon2  12258  restopn2  12263  cnpval  12278  cntop1  12281  cntop2  12282  cnprcl2k  12286  lmcvg  12297  iscnp4  12298  cnima  12300  cnco  12301  cnclima  12303  cnntri  12304  cnntr  12305  cnss1  12306  cnss2  12307  cncnpi  12308  cncnp  12310  cnrest  12315  cnrest2  12316  cnrest2r  12317  lmss  12326  lmres  12328  lmcn  12331  txuni2  12336  txbasex  12337  eltx  12339  txtop  12340  txtopon  12342  txopn  12345  txss12  12346  txbasval  12347  neitx  12348  txcnp  12351  upxp  12352  txcnmpt  12353  uptx  12354  txcn  12355  txrest  12356  txdis1cn  12358  txlm  12359  lmcn2  12360  cnmpt11  12363  cnmpt11f  12364  cnmpt1t  12365  cnmpt12  12367  cnmpt21  12371  cnmpt21f  12372  cnmpt2t  12373  cnmpt22  12374  cnmpt1res  12376  cnmpt2res  12377  cnmptcom  12378  imasnopn  12379  hmeocnv  12387  hmeoopn  12391  hmeocld  12392  hmeontr  12393  hmeoimaf1o  12394  hmeores  12395  txhmeo  12399  txswaphmeo  12401  xmet0  12443  blfvalps  12465  blfps  12489  blf  12490  blpnfctr  12519  xmetresbl  12520  isxms2  12532  xmstps  12537  msxms  12538  xmsxmet  12540  msmet  12541  xmspropd  12557  mspropd  12558  neibl  12571  bdxmet  12581  bdmopn  12584  mopnex  12585  xmetxp  12587  xmettxlem  12589  xmettx  12590  txmetcnp  12598  metcnpd  12600  cnmet  12610  unicntopcntop  12616  cnopncntop  12617  remetdval  12619  resubmet  12628  tgioo2cntop  12629  addcncntoplem  12631  divcnap  12635  fsumcncntop  12636  divccncfap  12657  cncfmet  12659  cncfcncntop  12660  cncfmptc  12662  cncfmptid  12663  cncfmpt1f  12664  cncfmpt2fcntop  12665  cdivcncfap  12667  negfcncf  12669  mulcncflem  12670  mulcncf  12671  cnopnap  12674  ivthinc  12701  ivthdec  12702  limcmpted  12712  limcimolemlt  12713  cnplimcim  12716  cnplimclemr  12718  cnlimcim  12720  cnlimc  12721  cnmptlimc  12723  limccnpcntop  12724  limccnp2lem  12725  limccnp2cntop  12726  reldvg  12728  dvfvalap  12730  dvcl  12732  dvbss  12734  dvfgg  12737  dvidlemap  12740  dvcnp2cntop  12743  dvcn  12744  dvaddxxbr  12745  dvmulxxbr  12746  dvaddxx  12747  dvmulxx  12748  dviaddf  12749  dvimulf  12750  dvcoapbr  12751  dvcjbr  12752  dvrecap  12757  dveflem  12766  dvef  12767  sincn  12769  coscn  12770  ex-or  12830  ex-an  12831  1kp2ke3k  12832  ex-exp  12835  ex-fac  12836  bj-2inf  13032  bj-inf2vnlem1  13064  subctctexmid  13092  nnsf  13095  peano3nninf  13097  nninfalllemn  13098  nninfself  13105  nninfsellemeqinf  13108  nninffeq  13112  trilpolemcl  13126  trilpolemisumle  13127  trilpolemeq1  13129  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator