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

Theorem eqid 2139
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 2136 1  |-  A  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1331    e. wcel 1480
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 1425  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  eqidd  2140  neirr  2317  sbsbc  2913  sbceqal  2964  dfnul2  3365  snidg  3554  prid1g  3627  tpid1  3634  tpid1g  3635  tpid2  3636  tpid2g  3637  tpid3  3639  dfiin2g  3846  eqbrtrid  3963  eqbrtrrid  3964  breqtrdi  3969  opabbii  3995  mpteq2ia  4014  mpteq2da  4017  sucidg  4338  onsucelsucexmidlem1  4443  regexmidlemm  4447  regexmidlem1  4448  reg2exmidlema  4449  regexmid  4450  reg2exmid  4451  reg3exmid  4494  tfisi  4501  finds1  4516  nn0suc  4518  nndceq0  4531  0elnn  4532  nnregexmid  4534  opelxp  4569  relopab  4666  relop  4689  ididg  4692  elrnmpt1s  4789  dfiun3g  4796  dfiin3g  4797  dmmptg  5036  funfn  5153  mpt0  5250  f0  5313  dffn4  5351  f1orn  5377  f1oabexg  5379  f1o00  5402  f1o0  5404  fnbrfvb  5462  fnrnfv  5468  funfvdm  5484  fvmptg  5497  fvmptd  5502  fvmpt2d  5507  fvmptdf  5508  mpteqb  5511  fvmptt  5512  funfvop  5532  eldmrexrn  5561  fvmptelrn  5573  fmpttd  5575  fmpt2d  5582  fmptco  5586  fmptcof  5587  fnasrn  5598  fnasrng  5600  mptexg  5645  eufnfv  5648  idref  5658  f1elima  5674  fliftrel  5693  fliftel  5694  fliftel1  5695  fliftcnv  5696  fliftf  5700  riotabiia  5747  acexmidlem2  5771  acexmidlemv  5772  oprabbii  5826  mpoeq12  5831  ovmpodxf  5896  ovmpodf  5902  ov6g  5908  f1ocnvd  5972  f1opw2  5976  suppssfv  5978  suppssov1  5979  ofvalg  5991  off  5994  offval2  5997  ofrfval2  5998  caofinvl  6004  abrexex  6015  abrexexg  6016  offres  6033  ofmres  6034  op1steq  6077  reldm  6084  mpoexga  6110  mpoex  6111  fnmpoovd  6112  fmpoco  6113  cnvf1o  6122  f1od2  6132  tposssxp  6146  brtpos2  6148  tpos0  6171  iunon  6181  tfrfun  6217  tfr2a  6218  tfrlemisucfn  6221  tfri1d  6232  tfr1onlemsucfn  6237  tfr1onlemubacc  6243  tfr1on  6247  tfri1dALT  6248  tfrcllemubacc  6256  tfrex  6265  rdgfun  6270  rdgon  6283  rdg0  6284  frec0g  6294  frecfnom  6298  freccllem  6299  freccl  6300  frecfcllem  6301  frecfcl  6302  frecsuclem  6303  0lt1o  6337  oafnex  6340  omfnex  6345  fnoei  6348  oeiexg  6349  oeiv  6352  oacl  6356  omcl  6357  oeicl  6358  oav2  6359  omv2  6361  eqer  6461  ecelqsg  6482  elqsn0m  6497  qsel  6506  qliftf  6514  ecoptocl  6516  eroprf  6522  ecopovsym  6525  ecopovtrn  6526  ecopovsymg  6528  ecopovtrng  6529  th3qlem2  6532  th3q  6534  mapsncnv  6589  mapsnf1o3  6591  mptelixpg  6628  ixpsnf1o  6630  en2d  6662  en3d  6663  dom2lem  6666  dom2  6669  1domsn  6713  xpcomen  6721  xpf1o  6738  mapxpen  6742  fidifsnen  6764  isbth  6855  elfir  6861  supsnti  6892  djueq1  6925  djueq2  6926  djuf1olem  6938  inl11  6950  updjud  6967  omp1eom  6980  difinfsn  6985  ctmlemr  6993  ctssdclemn0  6995  ctssdclemr  6997  ctssdc  6998  enumct  7000  nnnninf  7023  ismkvnex  7029  mkvprop  7032  exmidonfin  7055  exmidaclem  7069  exmidac  7070  cc3  7088  0npi  7133  indpi  7162  recidnq  7213  addnnnq0  7269  mulnnnq0  7270  genpprecll  7334  genppreclu  7335  caucvgprpr  7532  addsrpr  7565  mulsrpr  7566  0nsr  7569  00sr  7589  caucvgsrlemgt1  7615  opelreal  7647  eqresr  7656  axprecex  7700  nntopi  7714  axpre-suploc  7722  ltxrlt  7842  pncan3  7982  apreim  8377  divcanap2  8452  divcanap3  8470  lble  8717  sup3exmid  8727  nn1gt1  8766  0nn0  9004  pnf0xnn0  9059  0z  9077  decaddm10  9252  decmulnc  9260  10p10e20  9288  4t4e16  9292  5t4e20  9295  6t3e18  9298  6t4e24  9299  6t5e30  9300  7t3e21  9303  7t4e28  9304  7t5e35  9305  7t6e42  9306  7t7e49  9307  8t3e24  9309  8t4e32  9310  8t5e40  9311  8t7e56  9313  8t8e64  9314  9t3e27  9316  9t4e36  9317  9t5e45  9318  9t6e54  9319  9t7e63  9320  9t8e72  9321  9t9e81  9322  infrenegsupex  9401  znq  9428  ltpnf  9579  mnflt  9581  mnfltpnf  9583  xnegpnf  9623  xnegmnf  9624  xaddpnf1  9641  xaddpnf2  9642  xaddmnf1  9643  xaddmnf2  9644  pnfaddmnf  9645  mnfaddpnf  9646  lincmb01cmp  9798  iccf1o  9799  elfzuz2  9821  fseq1m1p1  9887  fz0tp  9913  flqdiv  10106  frec2uzzd  10185  frec2uzsucd  10186  frecuzrdgrrn  10193  frec2uzrdg  10194  frecuzrdgrcl  10195  frecuzrdgsuc  10199  frecuzrdgrclt  10200  frecuzrdgg  10201  frecuzrdgsuctlem  10208  uzenom  10210  fzfig  10215  nnenom  10219  seqeq1  10233  seq3val  10243  seqvalcd  10244  seqf  10246  seq3p1  10247  seqovcd  10248  seqp1cd  10251  seq3feq2  10255  seq3feq  10257  monoord2  10262  ser3mono  10263  seq3split  10264  seq3caopr2  10267  iseqf1olemqk  10279  seq3f1olemqsumkj  10283  seq3f1olemstep  10286  seq3f1oleml  10288  seq3f1o  10289  seq3homo  10295  seq3z  10296  seqfeq3  10297  seq3distr  10298  ser0f  10300  ser3ge0  10302  ser3le  10303  exp0  10309  0exp  10340  sq0  10395  sq10  10471  sq10e99m1  10472  facnn  10485  fac0  10486  bcval5  10521  hashinfom  10536  hashennn  10538  hashcl  10539  hashfz1  10541  hashen  10542  hash0  10555  fihashdom  10561  hashun  10563  seq3coll  10597  shftfibg  10604  shftfib  10607  shftfn  10608  2shfti  10615  seq3shft  10622  cvg1n  10770  resqrexlemsqa  10808  negfi  11011  xrmaxiflemcom  11030  xrmaxif  11032  infxrnegsupex  11044  climconst2  11072  climres  11084  climshft  11085  serclim0  11086  climle  11115  clim2ser  11118  clim2ser2  11119  climub  11125  climcvg1n  11131  climcaucn  11132  serf0  11133  sumfct  11155  fsum3cvg  11159  summodclem2  11163  zsumdc  11165  fsum3  11168  isumz  11170  fsumf1o  11171  isumss  11172  fsum3cvg2  11175  fsumsersdc  11176  fsum3ser  11178  fsumcl2lem  11179  fsumadd  11187  fsumsplitf  11189  sumsnf  11190  isummulc2  11207  isumadd  11212  fsumcnv  11218  mptfzshft  11223  fsumrev  11224  fsumshft  11225  fsummulc2  11229  iserabs  11256  isumshft  11271  isum1p  11273  isumlessdc  11277  divcnv  11278  trireciplem  11281  trirecip  11282  expcnvap0  11283  expcnvre  11284  expcnv  11285  explecnv  11286  geolim  11292  geolim2  11293  geo2lim  11297  geoisum  11298  geoisumr  11299  geoisum1  11300  geoisum1c  11301  cvgratnnlemseq  11307  cvgratz  11313  mertenslemub  11315  mertenslemi1  11316  mertenslem2  11317  mertensabs  11318  clim2prod  11320  clim2divap  11321  prodfap0  11326  prodfrecap  11327  prodfdivap  11328  prodeq2w  11337  fproddccvg  11353  prodmodclem2  11358  efcllemp  11376  efval  11379  eff  11381  efcvgfsum  11385  reefcl  11386  ege2le3  11389  ef0  11390  efcj  11391  efaddlem  11392  efadd  11393  eftlcl  11406  reeftlcl  11407  eftlub  11408  efsep  11409  effsumlt  11410  efgt1p2  11413  efgt1p  11414  eflegeo  11419  ef01bndlem  11474  sin01bnd  11475  cos01bnd  11476  eirraplem  11494  eirrap  11495  egt2lt3  11497  dvdsmul2  11527  odd2np1lem  11580  gcd0val  11660  gcd0id  11678  bezoutlemnewy  11695  eucalgcvga  11750  eucalg  11751  lcm0val  11757  qnumdencoprm  11882  qeqnumdivden  11883  phimul  11913  hashgcdeq  11915  xpnnen  11918  ennnfonelemk  11924  ennnfonelemj0  11925  ennnfonelem0  11929  ennnfonelemnn0  11946  ctinfom  11952  ctiunct  11964  ressid  12034  2strstr1g  12076  srngstrd  12095  ipsstrd  12114  elrest  12141  elrestr  12142  topnpropgd  12148  toptopon2  12200  toponmax  12206  tpstop  12216  tpspropd  12217  tsettps  12219  eltpsg  12221  tgiun  12256  ntrval  12293  clsval  12294  0cld  12295  uncld  12296  cldcls  12297  ntr0  12317  isopn3i  12318  neif  12324  neival  12326  neii2  12332  neiss  12333  opnneiss  12341  innei  12346  neissex  12348  tgrest  12352  stoig  12356  restco  12357  resttopon2  12361  restopn2  12366  cnpval  12381  cntop1  12384  cntop2  12385  cnprcl2k  12389  lmcvg  12400  iscnp4  12401  cnima  12403  cnco  12404  cnclima  12406  cnntri  12407  cnntr  12408  cnss1  12409  cnss2  12410  cncnpi  12411  cncnp  12413  cnrest  12418  cnrest2  12419  cnrest2r  12420  lmss  12429  lmres  12431  lmcn  12434  txuni2  12439  txbasex  12440  eltx  12442  txtop  12443  txtopon  12445  txopn  12448  txss12  12449  txbasval  12450  neitx  12451  txcnp  12454  upxp  12455  txcnmpt  12456  uptx  12457  txcn  12458  txrest  12459  txdis1cn  12461  txlm  12462  lmcn2  12463  cnmpt11  12466  cnmpt11f  12467  cnmpt1t  12468  cnmpt12  12470  cnmpt21  12474  cnmpt21f  12475  cnmpt2t  12476  cnmpt22  12477  cnmpt1res  12479  cnmpt2res  12480  cnmptcom  12481  imasnopn  12482  hmeocnv  12490  hmeoopn  12494  hmeocld  12495  hmeontr  12496  hmeoimaf1o  12497  hmeores  12498  txhmeo  12502  txswaphmeo  12504  xmet0  12546  blfvalps  12568  blfps  12592  blf  12593  blpnfctr  12622  xmetresbl  12623  isxms2  12635  xmstps  12640  msxms  12641  xmsxmet  12643  msmet  12644  xmspropd  12660  mspropd  12661  neibl  12674  bdxmet  12684  bdmopn  12687  mopnex  12688  xmetxp  12690  xmettxlem  12692  xmettx  12693  txmetcnp  12701  metcnpd  12703  cnmet  12713  unicntopcntop  12719  cnopncntop  12720  remetdval  12722  resubmet  12731  tgioo2cntop  12732  addcncntoplem  12734  divcnap  12738  fsumcncntop  12739  divccncfap  12760  cncfmet  12762  cncfcncntop  12763  cncfmptc  12765  cncfmptid  12766  cncfmpt1f  12767  cncfmpt2fcntop  12768  cdivcncfap  12770  negfcncf  12772  mulcncflem  12773  mulcncf  12774  cnopnap  12777  ivthinc  12804  ivthdec  12805  limcmpted  12815  limcimolemlt  12816  cnplimcim  12819  cnplimclemr  12821  cnlimcim  12823  cnlimc  12824  cnmptlimc  12826  limccnpcntop  12827  limccnp2lem  12828  limccnp2cntop  12829  reldvg  12831  dvfvalap  12833  dvcl  12835  dvbss  12837  dvfgg  12840  dvidlemap  12843  dvcnp2cntop  12846  dvcn  12847  dvaddxxbr  12848  dvmulxxbr  12849  dvaddxx  12850  dvmulxx  12851  dviaddf  12852  dvimulf  12853  dvcoapbr  12854  dvcjbr  12855  dvrecap  12860  dveflem  12870  dvef  12871  sincn  12873  coscn  12874  ex-or  13018  ex-an  13019  1kp2ke3k  13020  ex-exp  13023  ex-fac  13024  bj-2inf  13220  bj-inf2vnlem1  13252  subctctexmid  13280  nnsf  13285  peano3nninf  13287  nninfalllemn  13288  nninfself  13295  nninfsellemeqinf  13298  nninffeq  13302  trilpolemcl  13316  trilpolemisumle  13317  trilpolemeq1  13319  trilpolemlt1  13320
  Copyright terms: Public domain W3C validator