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

Theorem eqid 2177
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 171 . 2 (𝑥𝐴𝑥𝐴)
21eqriv 2174 1 𝐴 = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1353  wcel 2148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  eqidd  2178  neirr  2356  sbsbc  2966  sbceqal  3018  dfnul2  3424  snidg  3620  prid1g  3695  tpid1  3702  tpid1g  3703  tpid2  3704  tpid2g  3705  tpid3  3707  dfiin2g  3917  eqbrtrid  4035  eqbrtrrid  4036  breqtrdi  4041  opabbii  4067  mpteq2ia  4086  mpteq2da  4089  sucidg  4412  onsucelsucexmidlem1  4523  regexmidlemm  4527  regexmidlem1  4528  reg2exmidlema  4529  regexmid  4530  reg2exmid  4531  reg3exmid  4575  tfisi  4582  finds1  4597  nn0suc  4599  nndceq0  4613  0elnn  4614  nnregexmid  4616  opelxp  4652  relopab  4749  relop  4772  ididg  4775  elrnmpt1s  4872  dfiun3g  4879  dfiin3g  4880  dmmptg  5121  funfn  5241  mpt0  5338  f0  5401  dffn4  5439  f1orn  5466  f1oabexg  5468  f1o00  5491  f1o0  5493  fnbrfvb  5551  fnrnfv  5557  funfvdm  5574  fvmptg  5587  fvmptd  5592  fvmpt2d  5597  fvmptdf  5598  mpteqb  5601  fvmptt  5602  fnmptfvd  5615  funfvop  5623  eldmrexrn  5652  fvmptelcdm  5664  fmpttd  5666  fmpt2d  5673  fmptco  5677  fmptcof  5678  fnasrn  5689  fnasrng  5691  mptexg  5736  eufnfv  5741  idref  5751  f1elima  5767  fliftrel  5786  fliftel  5787  fliftel1  5788  fliftcnv  5789  fliftf  5793  riotabiia  5841  acexmidlem2  5865  acexmidlemv  5866  oprabbii  5923  mpoeq12  5928  ovmpodxf  5993  ovmpodf  5999  ov6g  6005  f1ocnvd  6066  f1opw2  6070  suppssfv  6072  suppssov1  6073  ofvalg  6085  off  6088  offval2  6091  ofrfval2  6092  caofinvl  6098  mptexw  6107  abrexex  6111  abrexexg  6112  offres  6129  ofmres  6130  op1steq  6173  reldm  6180  mpoexga  6206  mpoexw  6207  mpoex  6208  fnmpoovd  6209  fmpoco  6210  cnvf1o  6219  f1od2  6229  tposssxp  6243  brtpos2  6245  tpos0  6268  iunon  6278  tfrfun  6314  tfr2a  6315  tfrlemisucfn  6318  tfri1d  6329  tfr1onlemsucfn  6334  tfr1onlemubacc  6340  tfr1on  6344  tfri1dALT  6345  tfrcllemubacc  6353  tfrex  6362  rdgfun  6367  rdgon  6380  rdg0  6381  frec0g  6391  frecfnom  6395  freccllem  6396  freccl  6397  frecfcllem  6398  frecfcl  6399  frecsuclem  6400  0lt1o  6434  oafnex  6438  omfnex  6443  fnoei  6446  oeiexg  6447  oeiv  6450  oacl  6454  omcl  6455  oeicl  6456  oav2  6457  omv2  6459  eqer  6560  ecelqsg  6581  elqsn0m  6596  qsel  6605  qliftf  6613  ecoptocl  6615  eroprf  6621  ecopovsym  6624  ecopovtrn  6625  ecopovsymg  6627  ecopovtrng  6628  th3qlem2  6631  th3q  6633  mapsncnv  6688  mapsnf1o3  6690  mptelixpg  6727  ixpsnf1o  6729  en2d  6761  en3d  6762  dom2lem  6765  dom2  6768  1domsn  6812  xpcomen  6820  xpf1o  6837  mapxpen  6841  fidifsnen  6863  isbth  6959  elfir  6965  supsnti  6997  djueq1  7032  djueq2  7033  djuf1olem  7045  inl11  7057  updjud  7074  omp1eom  7087  difinfsn  7092  ctmlemr  7100  ctssdclemn0  7102  ctssdclemr  7104  ctssdc  7105  enumct  7107  infnninf  7115  nnnninf  7117  nnnninfeq  7119  nninfisollemne  7122  nninfisol  7124  ismkvnex  7146  mkvprop  7149  nninfwlporlemd  7163  nninfwlpoimlemginf  7167  exmidonfin  7186  exmidaclem  7200  exmidac  7201  cc3  7245  0npi  7290  indpi  7319  recidnq  7370  addnnnq0  7426  mulnnnq0  7427  genpprecll  7491  genppreclu  7492  caucvgprpr  7689  addsrpr  7722  mulsrpr  7723  0nsr  7726  00sr  7746  caucvgsrlemgt1  7772  opelreal  7804  eqresr  7813  axprecex  7857  nntopi  7871  axpre-suploc  7879  ltxrlt  8000  pncan3  8142  apreim  8537  divcanap2  8613  divcanap3  8631  lble  8880  sup3exmid  8890  nn1gt1  8929  0nn0  9167  pnf0xnn0  9222  0z  9240  decaddm10  9418  decmulnc  9426  10p10e20  9454  4t4e16  9458  5t4e20  9461  6t3e18  9464  6t4e24  9465  6t5e30  9466  7t3e21  9469  7t4e28  9470  7t5e35  9471  7t6e42  9472  7t7e49  9473  8t3e24  9475  8t4e32  9476  8t5e40  9477  8t7e56  9479  8t8e64  9480  9t3e27  9482  9t4e36  9483  9t5e45  9484  9t6e54  9485  9t7e63  9486  9t8e72  9487  9t9e81  9488  infrenegsupex  9570  znq  9600  ltpnf  9754  mnflt  9757  mnfltpnf  9759  xnegpnf  9802  xnegmnf  9803  xaddpnf1  9820  xaddpnf2  9821  xaddmnf1  9822  xaddmnf2  9823  pnfaddmnf  9824  mnfaddpnf  9825  lincmb01cmp  9977  iccf1o  9978  iccen  9980  elfzuz2  10002  fseq1m1p1  10068  fz0tp  10095  fz0to4untppr  10097  flqdiv  10294  frec2uzzd  10373  frec2uzsucd  10374  frecuzrdgrrn  10381  frec2uzrdg  10382  frecuzrdgrcl  10383  frecuzrdgsuc  10387  frecuzrdgrclt  10388  frecuzrdgg  10389  frecuzrdgsuctlem  10396  uzenom  10398  fzfig  10403  nnenom  10407  seqeq1  10421  seq3val  10431  seqvalcd  10432  seqf  10434  seq3p1  10435  seqovcd  10436  seqp1cd  10439  seq3feq2  10443  seq3feq  10445  monoord2  10450  ser3mono  10451  seq3split  10452  seq3caopr2  10455  iseqf1olemqk  10467  seq3f1olemqsumkj  10471  seq3f1olemstep  10474  seq3f1oleml  10476  seq3f1o  10477  seq3homo  10483  seq3z  10484  seqfeq3  10485  seq3distr  10486  ser0f  10488  ser3ge0  10490  ser3le  10491  exp0  10497  0exp  10528  sq0  10583  sq10  10663  sq10e99m1  10664  facnn  10678  fac0  10679  bcval5  10714  hashinfom  10729  hashennn  10731  hashcl  10732  hashfz1  10734  hashen  10735  hash0  10747  fihashdom  10754  hashun  10756  seq3coll  10793  shftfibg  10800  shftfib  10803  shftfn  10804  2shfti  10811  seq3shft  10818  cvg1n  10966  resqrexlemsqa  11004  negfi  11207  xrmaxiflemcom  11228  xrmaxif  11230  infxrnegsupex  11242  climconst2  11270  climres  11282  climshft  11283  serclim0  11284  climle  11313  clim2ser  11316  clim2ser2  11317  climub  11323  climcvg1n  11329  climcaucn  11330  serf0  11331  sumfct  11353  fsum3cvg  11357  summodclem2  11361  zsumdc  11363  fsum3  11366  isumz  11368  fsumf1o  11369  isumss  11370  fsum3cvg2  11373  fsumsersdc  11374  fsum3ser  11376  fsumcl2lem  11377  fsumadd  11385  fsumsplitf  11387  sumsnf  11388  isummulc2  11405  isumadd  11410  fsumcnv  11416  mptfzshft  11421  fsumrev  11422  fsumshft  11423  fsummulc2  11427  iserabs  11454  isumshft  11469  isum1p  11471  isumlessdc  11475  divcnv  11476  trireciplem  11479  trirecip  11480  expcnvap0  11481  expcnvre  11482  expcnv  11483  explecnv  11484  geolim  11490  geolim2  11491  geo2lim  11495  geoisum  11496  geoisumr  11497  geoisum1  11498  geoisum1c  11499  cvgratnnlemseq  11505  cvgratz  11511  mertenslemub  11513  mertenslemi1  11514  mertenslem2  11515  mertensabs  11516  clim2prod  11518  clim2divap  11519  prodfap0  11524  prodfrecap  11525  prodfdivap  11526  prodeq2w  11535  fproddccvg  11551  prodmodclem2  11556  zproddc  11558  fprodseq  11562  fprodntrivap  11563  prod1dc  11565  prodfct  11566  fprodf1o  11567  prodssdc  11568  fprodssdc  11569  fprodmul  11570  prodsnf  11571  fprodshft  11597  fprodrev  11598  fprodcnv  11604  efcllemp  11637  efval  11640  eff  11642  efcvgfsum  11646  reefcl  11647  ege2le3  11650  ef0  11651  efcj  11652  efaddlem  11653  efadd  11654  eftlcl  11667  reeftlcl  11668  eftlub  11669  efsep  11670  effsumlt  11671  efgt1p2  11674  efgt1p  11675  eflegeo  11680  ef01bndlem  11735  sin01bnd  11736  cos01bnd  11737  eirraplem  11755  eirrap  11756  egt2lt3  11758  dvdsmul2  11792  odd2np1lem  11847  nninfdcex  11924  zsupssdc  11925  gcd0val  11931  gcd0id  11950  bezoutlemnewy  11967  nnmindc  12005  nnminle  12006  eucalgcvga  12028  eucalg  12029  lcm0val  12035  qnumdencoprm  12163  qeqnumdivden  12164  phimul  12196  eulerthlemh  12201  eulerthlemth  12202  prmdivdiv  12207  hashgcdeq  12209  phisum  12210  odzval  12211  powm2modprm  12222  reumodprminv  12223  pythagtriplem18  12251  pcpremul  12263  pceulem  12264  pceu  12265  pczpre  12267  pczcl  12268  pcmul  12271  pcdiv  12272  pc1  12275  pczdvds  12283  pczndvds  12285  pczndvds2  12287  pcneg  12294  infpn  12329  1arithlem2  12332  1arith  12335  4sqlem3  12358  mul4sq  12362  xpnnen  12365  ennnfonelemk  12371  ennnfonelemj0  12372  ennnfonelem0  12376  ennnfonelemnn0  12393  ctinfom  12399  ctiunct  12411  ssnnct  12418  nninfdclemcl  12419  nninfdclemf  12420  nninfdclemp1  12421  2strstr1g  12546  ressplusgd  12553  srngstrd  12566  ipsstrd  12588  elrest  12630  elrestr  12631  topnpropgd  12637  mgmsscl  12659  plusffng  12663  mgmplusf  12664  mgmb1mgm1  12666  mgm0  12667  mgm1  12668  opifismgmdc  12669  grpidpropdg  12672  0g0  12674  mgmidcl  12676  mgmlrid  12677  grpidd  12681  sgrpmgm  12692  sgrp0  12694  sgrp1  12695  sgrpidmndm  12700  mndsgrp  12701  mndidcl  12710  mndbn0  12711  hashfinmndnn  12712  ismndd  12717  mndpfo  12718  mndfo  12719  mndpropd  12720  issubmnd  12722  mnd1  12724  mhmf  12733  mhmpropd  12734  mhmlin  12735  mhm0  12736  idmhm  12737  mhmf1o  12738  issubm2  12741  mndissubm  12743  submss  12744  submid  12745  subm0cl  12746  submcl  12747  0subm  12748  insubm  12749  0mhm  12750  mhmco  12751  mhmima  12752  mhmeql  12753  grpmnd  12761  grppropd  12770  isgrpd2e  12773  dfgrp2  12779  grpbn0  12782  grpn0  12785  grprcan  12787  grpidd2  12791  grpinvval  12793  grpinvfng  12794  grpsubval  12796  grpinvf  12797  grplrinv  12804  grpidinv  12806  grpinvid  12807  grplcan  12808  grpasscan1  12809  grpasscan2  12810  grpinvinv  12813  grpinvcnv  12814  grplmulf1o  12820  grpinvpropdg  12821  grpidssd  12822  grpinvssd  12823  grpinvadd  12824  grpsubf  12825  grpsubrcan  12827  grpinvsub  12828  grpinvval2  12829  grpsubid  12830  grpsubid1  12831  grpsubeq0  12832  grpsubadd0sub  12833  grpsubadd  12834  grpsubsub  12835  grpaddsubass  12836  grppncan  12837  grpnpcan  12838  grpnnncan2  12843  dfgrp3m  12845  grplactcnv  12848  grplactf1o  12849  grpsubpropdg  12850  grpsubpropd2  12851  grp1  12852  grp1inv  12853  mhmid  12855  mhmmnd  12856  mhmfmhm  12857  ghmgrp  12858  mulgfng  12863  mulg0  12864  mulgnn  12865  mulg1  12866  mulgnnp1  12867  mulgnegnn  12869  mulgnn0p1  12870  mulgnnsubcl  12871  mulgnncl  12874  mulgnn0cl  12875  mulgcl  12876  mulgneg  12877  mulgaddcomlem  12881  mulgaddcom  12882  mulginvcom  12883  mulgnn0z  12885  mulgz  12886  mulgnndir  12887  mulgnn0dir  12888  mulgdirlem  12889  mulgdir  12890  mulgneg2  12892  mulgnnass  12893  mulgnn0ass  12894  mulgass  12895  mulgmodid  12897  mulgsubdir  12898  mhmmulg  12899  mulgpropdg  12900  submmulgcl  12901  cmnpropd  12912  iscmnd  12915  cmnmnd  12918  ablsub2inv  12928  ablsub4  12930  abladdsub4  12931  ablpncan2  12933  ablsubsub4  12936  ablpnpcan  12937  ablnncan  12938  ablsub32  12939  ablnnncan  12940  ablsubsub23  12942  subcmnd  12943  mgpex  12949  mgpbasg  12950  mgpscag  12951  mgptsetg  12952  mgptopng  12953  mgpdsg  12954  dfur2g  12958  srgcmn  12962  srgmgp  12964  srgdilem  12965  srgcl  12966  srgass  12967  srgideu  12968  srgidcl  12972  srgidmlem  12974  issrgid  12977  srgrz  12980  srglz  12981  srg1zr  12983  srgmulgass  12985  srgpcomp  12986  srgpcompp  12987  srgpcomppsc  12988  srglmhm  12989  srgrmhm  12990  srg1expzeq1  12991  ringgrp  12997  ringmgp  12998  crngring  13004  mgpf  13007  ringdilem  13008  ringcl  13009  crngcom  13010  iscrng2  13011  ringass  13012  ringideu  13013  ringidcl  13016  ringidmlem  13018  isringid  13021  ringid  13022  ringidss  13025  ringcom  13027  ringabl  13028  ringpropd  13030  crngpropd  13031  isringd  13033  iscrngd  13034  ringlz  13035  ringrz  13036  ringsrg  13037  ring1eq0  13038  ringnegl  13041  rngnegr  13042  ringmneg1  13043  ringmneg2  13044  ringsubdi  13046  rngsubdir  13047  mulgass2  13048  ring1  13049  ringn0  13050  opprex  13057  opprsllem  13058  opprring  13061  opprringbg  13062  oppr0g  13063  oppr1g  13064  opprnegg  13065  mulgass3  13066  reldvdsrsrg  13073  dvdsrvald  13074  dvdsrd  13075  dvdsrmuld  13077  dvdsrex  13079  dvdsrcl2  13080  dvdsrid  13081  dvdsrtr  13082  dvdsrneg  13084  dvdsr01  13085  dvdsr02  13086  1unit  13088  opprunitd  13091  crngunit  13092  dvdsunit  13093  unitmulcl  13094  unitmulclb  13095  unitgrpbasd  13096  unitgrp  13097  unitabl  13098  unitgrpid  13099  unitsubm  13100  invrfvald  13103  unitinvcl  13104  unitinvinv  13105  unitlinv  13107  unitrinv  13108  1rinv  13109  0unit  13110  unitnegcl  13111  toptopon2  13150  toponmax  13156  tpstop  13166  tpspropd  13167  tsettps  13169  eltpsg  13171  tgiun  13206  ntrval  13243  clsval  13244  0cld  13245  uncld  13246  cldcls  13247  ntr0  13267  isopn3i  13268  neif  13274  neival  13276  neii2  13282  neiss  13283  opnneiss  13291  innei  13296  neissex  13298  tgrest  13302  stoig  13306  restco  13307  resttopon2  13311  restopn2  13316  cnpval  13331  cntop1  13334  cntop2  13335  cnprcl2k  13339  lmcvg  13350  iscnp4  13351  cnima  13353  cnco  13354  cnclima  13356  cnntri  13357  cnntr  13358  cnss1  13359  cnss2  13360  cncnpi  13361  cncnp  13363  cnrest  13368  cnrest2  13369  cnrest2r  13370  lmss  13379  lmres  13381  lmcn  13384  txuni2  13389  txbasex  13390  eltx  13392  txtop  13393  txtopon  13395  txopn  13398  txss12  13399  txbasval  13400  neitx  13401  txcnp  13404  upxp  13405  txcnmpt  13406  uptx  13407  txcn  13408  txrest  13409  txdis1cn  13411  txlm  13412  lmcn2  13413  cnmpt11  13416  cnmpt11f  13417  cnmpt1t  13418  cnmpt12  13420  cnmpt21  13424  cnmpt21f  13425  cnmpt2t  13426  cnmpt22  13427  cnmpt1res  13429  cnmpt2res  13430  cnmptcom  13431  imasnopn  13432  hmeocnv  13440  hmeoopn  13444  hmeocld  13445  hmeontr  13446  hmeoimaf1o  13447  hmeores  13448  txhmeo  13452  txswaphmeo  13454  xmet0  13496  blfvalps  13518  blfps  13542  blf  13543  blpnfctr  13572  xmetresbl  13573  isxms2  13585  xmstps  13590  msxms  13591  xmsxmet  13593  msmet  13594  xmspropd  13610  mspropd  13611  neibl  13624  bdxmet  13634  bdmopn  13637  mopnex  13638  xmetxp  13640  xmettxlem  13642  xmettx  13643  txmetcnp  13651  metcnpd  13653  cnmet  13663  unicntopcntop  13669  cnopncntop  13670  remetdval  13672  resubmet  13681  tgioo2cntop  13682  addcncntoplem  13684  divcnap  13688  fsumcncntop  13689  divccncfap  13710  cncfmet  13712  cncfcncntop  13713  cncfmptc  13715  cncfmptid  13716  cncfmpt1f  13717  cncfmpt2fcntop  13718  cdivcncfap  13720  negfcncf  13722  mulcncflem  13723  mulcncf  13724  cnopnap  13727  ivthinc  13754  ivthdec  13755  limcmpted  13765  limcimolemlt  13766  cnplimcim  13769  cnplimclemr  13771  cnlimcim  13773  cnlimc  13774  cnmptlimc  13776  limccnpcntop  13777  limccnp2lem  13778  limccnp2cntop  13779  reldvg  13781  dvfvalap  13783  dvcl  13785  dvbss  13787  dvfgg  13790  dvidlemap  13793  dvcnp2cntop  13796  dvcn  13797  dvaddxxbr  13798  dvmulxxbr  13799  dvaddxx  13800  dvmulxx  13801  dviaddf  13802  dvimulf  13803  dvcoapbr  13804  dvcjbr  13805  dvrecap  13810  dveflem  13820  dvef  13821  sincn  13823  coscn  13824  lgsfcl  14042  lgsfle1  14043  lgsval4lem  14045  lgscl2  14046  lgs0  14047  lgscl  14048  lgsle1  14049  lgsval2  14050  lgs2  14051  lgsval4  14054  lgsfcl3  14055  lgsneg  14058  lgsmod  14060  lgsdirprm  14068  lgsdir  14069  lgsdi  14071  lgsne0  14072  2sqlem9  14093  ex-or  14096  ex-an  14097  1kp2ke3k  14098  ex-exp  14101  ex-fac  14102  fnmptd  14178  bj-2inf  14312  bj-inf2vnlem1  14344  subctctexmid  14373  nnsf  14377  peano3nninf  14379  nninfself  14385  nninfsellemeqinf  14388  nninffeq  14392  iooreen  14406  trilpolemcl  14408  trilpolemisumle  14409  trilpolemeq1  14411  trilpolemlt1  14412  iswomni0  14422  dceqnconst  14430  dcapnconst  14431  nconstwlpolemgt0  14434
  Copyright terms: Public domain W3C validator