Theorem eqid 1518

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, Book VII, Part 17). (Thanks to Stefan Allan for this information.)

Assertion

Ref	Expression
eqid	⊢ A = A

Proof of Theorem eqid

Step	Hyp	Ref	Expression
1		biid 168	. 2 ⊢ (x ∈ A ↔ x ∈ A)
2	1	eqriv 1515	1 ⊢ A = A

Syntax hints:   = wceq 992   ∈ wcel 994

This theorem is referenced by:  eqidd 1519  visset 1859  reu3 1977  sbcbii 2026  ssid 2132  uniiunlem 2184  dfnul2 2334  dfnul3 2335  noel 2336  npss0 2362  ifor 2435  snidg 2494  prid1g 2511  snsspr1 2534  int0 2614  syl5eqbr 2721  syl5eqbrr 2722  syl6breq 2727  ssbri 2730  opabbii 2745  so 2943  nlim0 3031  ordun 3071  unisn2 3098  ralxfrALT 3123  finds1 3247  relop 3365  ididg 3368  issetid 3370  dm0 3414  dmi 3415  xp11a 3562  xp11b 3563  funfn 3647  f0 3763  dffn4 3785  f1orn 3806  f1oabexg 3808  f1o00 3825  f1o0 3827  funbrfvb 3866  dffn5 3869  funfv 3881  fvco 3885  fvopab4g 3890  fvopab4gf 3892  eqfnfvALT 3910  fvimacnvALT 3923  fopabcos 3947  fopabsn 3954  funiunfv 3980  oprabbii 4056  oprabval2gf 4086  oprabval3 4090  oprabval6g 4093  1st2val 4158  2nd2val 4159  curry1 4193  curry1f 4194  curry1val 4195  curry2 4196  curry2f 4197  curry2val 4198  tfr1 4225  tfr2 4226  tfr3 4227  tz7.44-1 4229  rdglem1 4238  0lt1o 4283  oe0m 4293  oawordeu 4325  nneob 4395  ecelqsi 4432  ecoptocl 4444  ecopoprsym 4451  ecopoprtrn 4452  th3qlem2 4456  th3q 4458  en2d 4541  en2 4543  en3 4544  dom2d 4545  dom2 4546  pw2en 4587  ac6sfilem3 4590  sbth 4602  mapen 4638  mapxpen 4642  xpmapenlem4 4646  xpmapen 4648  unbnn 4690  unfilem3 4696  abfii3 4706  iunfi 4712  pwfi 4714  inf0 4751  inf3 4765  infeq5 4766  tz9.1 4792  tz9.12 4808  ssrankr1 4822  rankel 4826  rankpw 4830  r1rankid 4840  scott0 4863  cplem2 4867  aceq3 4879  aceq4 4880  aceq5 4886  aceq6a 4887  aceq6b 4888  ac6 4901  aceqkm 4927  numth 4930  weth 4933  zorn2lem6 4939  zornlem 4941  zorn2 4942  brdom7disj 4950  brdom6disj 4951  iundom 4958  cardsn 4982  unxpdomlem 4993  alephfp2 5051  dominf 5054  0npi 5164  recidpq 5225  0npr 5250  genpprecl 5258  00sr 5362  opelreal 5403  eqresr 5409  ltsor 5415  pncan3 5531  leid 5685  renfdisj 5693  ltpnf 5696  mnflt 5697  mnfltpnf 5698  xrleid 5714  divcan2i 5868  nnleltp1 6100  0nn0 6281  0z 6314  uzwo3 6390  zmin 6391  znq 6397  fldiv 6456  icoshftf1o 6538  seq11 6682  seq1p1 6683  seq1fn 6685  shftfn 6708  shftval 6711  seqzres2 6756  dfseq0 6758  exp0 6766  0exp 6784  sq0 6832  discrlem2 6858  discrlem 6860  sqrlem21 6894  sqrmsqi 6910  replim 6962  abs0 7080  fsum1i 7208  fsump1i 7209  climsub 7333  climcmp 7341  caucvg2i 7368  caucvg3i 7370  iserzabsi 7382  cvgcmp2i 7384  cvgcmp2ci 7387  cvgcmp3cei 7391  isumclim5 7406  isumshfti 7408  isumshft2i 7409  isummulc1 7416  isummulc1iALT 7417  infcvgaux1i 7423  infcvgaux2i 7424  infcvgi 7428  explecnv 7438  geolimi 7441  geolim 7442  geolim1i 7443  geolim1 7444  geosumi 7446  geoisum 7447  geoisum1 7449  geoisum1c 7450  cvgratlem5 7459  cvgrati 7460  divccncf 7485  ivthlem8 7493  isupivthi 7495  dsupivthi 7497  efseq1ex 7511  dfef2i 7512  efcl 7517  efcvgfsum 7520  reefcli 7522  erelem2 7525  erelem6 7529  ereALT 7536  ege2 7537  ele3 7538  ege2le3 7539  ef0 7540  efcji 7541  efaddlem23 7565  efaddlem27 7569  efaddlem28 7570  efaddi 7571  eftlex 7583  ef1tlubi 7587  ef01tllem2 7589  ef01tllem2OLD 7590  ef01tlubi 7591  absef01tlubi 7593  eirrlem3 7596  eirr 7599  ef4pi 7607  ef4p 7608  efge1i 7609  efge1pi 7610  absefm1lei 7620  eflegeoi 7623  efcnlem3 7629  reeff1olem2 7633  sin01bndlem2 7677  cos01bndlem2 7679  sin01bnd 7681  cos01bnd 7682  acdc3 7698  acdc2lem2 7701  acdc2 7702  acdc5lem2 7704  acdc5 7705  acdc 7707  acdcALT 7708  nnenom 7710  qnnen 7715  unben 7717  infpn 7720  ruclem15 7736  ruclem38 7759  infxpidmlem9 7772  infxpidm 7776  infmap2 7793  eltopsp 7816  tpsex 7817  istps2 7819  basgen2 7851  ntrval 7886  clsval 7887  0cld 7888  iincld 7889  uncld 7891  cldcls 7892  cls0 7919  ntr0 7920  neival 7927  neii2 7932  neiss 7933  opnneiss 7942  innei 7946  neissex 7948  lpval 7953  qdensere 7961  cnpval 7969  cnpimaex 7975  cnima 7977  cnco 7978  cnpco 7979  cnclima 7981  haustop 7996  dfms2 8009  met0 8025  metres 8033  metxpcl 8042  metxplem4 8043  metxp 8044  blfval 8045  blval 8047  blrn 8051  blf 8054  blelrn 8058  blss 8063  opni 8074  opni2 8075  opni3 8076  blssopn 8077  opnuni 8078  opnin 8079  unirnbl 8085  neibl 8087  lpbl 8090  methausi 8092  methaus 8093  metcnpf 8094  metcnf 8095  metcnconst 8096  metcnp 8098  metcn 8100  metcnss 8109  metcnss2 8110  metidcn 8111  metdnsconst 8112  cncfmet 8116  remetdval 8119  remet 8121  tgioo 8126  rehaus 8128  lmrel 8138  lmbr 8139  lmuni 8162  lmsslem 8163  lmss 8164  caussi 8165  causs 8166  lmfex 8170  cmsmet 8172  metelcls 8176  metcld 8178  metcn4 8182  metcn4i 8183  oprcn 8188  opr1cn 8189  opr2cn 8190  opr1scn 8191  addcn 8197  subcn 8198  mulcn 8199  fsumcnlem 8200  fsumcn 8201  iscms2 8205  lmcau 8207  cmsss 8208  bcthlem32 8241  bcth 8243  grprndm 8267  0ngrp 8268  grprn 8269  grpidval 8275  grprcan 8280  grpinvval 8284  grpinvcl 8285  grpinvid 8291  grplcan 8292  grpasscan1 8294  grpasscan2 8295  grp2inv 8296  grpinvf 8297  grpinvop 8298  grpdivfval 8299  grpdivval 8300  grpdivf 8303  grpdivdiv 8305  grpmuldivass 8306  grpdivid 8307  grppncan 8308  grpnpcan 8309  grppnpcan2 8310  grpnnncan2 8311  gxoprval 8313  gxval 8314  gxpval 8315  gxnval 8316  gx0 8317  gxnn0neg 8319  gxnn0suc 8320  gxcl 8321  gxcom 8325  gxinv 8326  gxsuc 8328  gxid 8329  gxnn0add 8330  gxadd 8331  gxnn0mul 8333  gxmul 8334  resgrprn 8336  grplactval 8338  grplactf1o 8339  ablgrp 8343  abldivdiv4 8350  ablnncan 8353  gxdi 8355  subgres 8359  subgid 8362  subgabl 8365  cnid 8368  addinv 8369  readdsubg 8370  zaddsubg 8371  mulid 8373  ghgrpi 8378  ringabl 8392  vcabl 8423  vcm 8437  vcrinv 8438  vclinv 8439  vcoprnelem 8444  vcoprne 8445  vcex 8446  cnvc 8449  nvvop 8475  nvex 8477  nvvc 8481  nvabl 8482  nvsf 8485  nvscl 8494  nvsid 8495  nvsass 8496  nvdi 8498  nvdir 8499  nv2 8500  vsfval 8501  nvzcl 8502  nv0 8505  nvsz 8506  nvinv 8507  invfval 8508  nvmval 8510  nvmfval 8511  nvzs 8512  nvmf 8513  nvnnncan1 8515  nvnnncan2 8516  nvmdi 8517  nvnegneg 8518  nvrinv 8520  nvlinv 8521  nvsubadd 8522  nvpncan2 8523  nvaddsub4 8528  nvsubsub23 8529  nvnncan 8530  nvmeq0 8531  nvmid 8532  nvf 8533  nvdm 8536  nvs 8537  nvsub 8542  nvz0 8543  nvz 8544  nvtri 8545  nvmtri 8546  nvmtri2 8547  nvabs 8548  nvge0 8549  nvop 8552  nvoprne 8553  cnnvg 8555  cnnvba 8556  cnnvdemo 8557  cnnvs 8558  cnnvnm 8559  cnnvm 8560  elimnvu 8562  imsdval2 8565  nvnd 8566  imsdf 8567  imsmet 8571  nvelbl 8572  nvelbl2 8573  nvcnf 8574  nvcnpf 8575  nvcni 8576  nvcni2 8577  nvcni3 8578  nvlmcl 8579  nvlmle 8580  cnims 8581  vacnlem3 8584  vacn 8588  sqcn 8589  sqcn2 8590  nmcni 8592  nmcn 8593  nmcn2 8594  nmcn3 8595  nmcnc 8596  abscn 8597  abscncfALT 8598  va1cnlem 8599  va1cn 8600  sm1cnilem 8601  sm1cni 8602  ipfval 8606  ipval 8607  ipid 8617  ipcl 8619  ipf 8620  ipcj 8621  ip0r 8624  ipz 8626  ip1cnilem2 8628  ip1cnilem3 8629  ip1cnilem4 8630  ip1cnilem5 8631  ip1cni 8633  sspval 8636  sspid 8638  sspnv 8639  sspba 8640  sspg 8641  ssps 8643  sspmlem 8645  sspmval 8646  sspm 8647  sspz 8648  sspn 8649  sspival 8651  sspi 8652  sspimsval 8653  sspims 8654  lnoval 8667  lnof 8670  lno0 8671  lnocoi 8672  lnoadd 8673  lnosub 8674  lnomul 8675  nvcnpi3 8676  nvcnpi4 8677  nvo00 8678  nmoval 8680  nmosetn0 8682  nmoxr 8683  nmoge0 8684  nmorepnf 8685  nmolb 8688  isblo2 8698  bloln 8699  blof 8700  nmblore 8701  0oo 8704  0lno 8705  nmo0 8706  0blo 8707  nmlno0i 8709  nmlno0 8710  nmlnoubi 8711  nmlnogt0 8712  lnon0 8713  nmblolbii 8714  nmblolbi 8715  isblo3i 8716  blometi 8718  blocnilem 8719  blocni 8720  blocn 8722  blocn2 8723  phop 8733  cnph 8734  elimphu 8736  isph 8737  ip0i 8740  ip1i 8742  ip2i 8743  ipdirilem 8744  ipdiri 8745  ipasslem1 8746  ipasslem2 8747  ipasslem6 8751  ipasslem7 8752  ipasslem8 8753  ipasslem9 8754  ipasslem11 8756  ipassi 8757  ipdir 8758  ipass 8761  ipsubdir 8764  siii 8769  sii 8770  sspph 8771  ipblnfi 8772  ip2eqi 8773  ajfuni 8776  ajfun 8777  ajval 8778  bnnv 8783  bnsscmcl 8785  cnbn 8786  ubthlem3 8789  ubthlem4 8790  ubthlem6 8792  ubthlem9 8795  ubthlem11 8797  ubthlem12 8798  ubthlem12OLD 8799  ubthlem13 8800  ubthlem13OLD 8801  ubthlem14 8802  ubthii 8803  ubthi 8804  minveclem1 8805  minveclem2 8806  minveclem3 8807  minveclem9 8813  minveclem16 8820  minveclem21 8825  minveclem23 8827  minveclem28 8832  minveclem29 8833  minveclem33 8837  minvecex 8838  minveclem37 8841  minveceu 8843  minvecex2 8848  hlipgt0 8878  hlcompl 8879  htthlem4 8885  htthlem5 8886  htthlem12 8893  htthi 8894  pstr 8914  spwval2 8915  spwval 8921  spwnex 8923  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  spwpr4c 8928  sincnlem 8933  sincn 8936  coscn 8937  pilem2 8939  pilem3 8940  pilem4 8941  sineq0 8983  sineq0OLD 8984  efghgrpilem 8991  efghgrpi 8992  efifolem1 8994  efifolem4 8997  shftefif1o 9014  eff1oi 9018  eff1o 9020  h2hva 9118  h2hsm 9119  h2hnm 9120  h2hvs 9121  axhcompl 9143  hiidrcl 9237  normlem7 9258  norm-ii.i 9280  hilid 9304  hilvc 9305  hilnormi 9306  hhba 9310  hh0v 9311  hhims 9315  hhims2 9316  hhip 9320  hhph 9321  bcsiHIL 9323  hilmet 9337  hilmetdval 9338  hilmetba 9339  hhhl 9349  hilcms 9350  hilhl 9351  hhssva 9405  hhsssm 9406  hhssnm 9407  hhssabli 9408  hhssnv 9410  hhssnvt 9411  hhsst 9412  hhshsslem1 9413  hhshsslem2 9414  hhsssh 9415  hhsssh2 9416  hhssba 9417  hhssvs 9418  hhssph 9420  hhssims 9421  hhssims2 9422  hhssbn 9427  occllem7 9455  projlem8 9469  projlem10 9471  projlem31 9492  projlem 9493  projlemHIL 9494  pjthlem13 9507  pjthi 9509  pjval 9515  shsva 9560  hosval 9792  hosvalOLD 9793  homval 9794  hodval 9795  hodvalOLD 9796  hfsval 9797  hfmval 9798  pjcompi 9897  mayetes3i 9953  hoaddcl 9964  homulcl 9965  hodseqi 10000  nmopsetretHIL 10071  nmopsetn0 10072  nmfnsetn0 10085  hhlnoi 10106  hhbloi 10108  hh0oi 10109  nmoplb 10111  nmopub2tHIL 10114  nmfnlb 10128  bravalval 10148  brafn 10151  kbop 10157  kbvalval 10158  eigval1 10164  hmopbdopiHIL 10191  nmlnop0iHIL 10200  nmcopexi 10236  nmcfnexi 10265  cnlnadji 10288  nmopadjlei 10300  kbass2 10330  kbass5 10333  leopsq 10342  hmopidmch 10361  hmopidmpj 10362  stri 10465  hstri 10473  goeqi 10481  irredi 10603  mdsymlem8 10619  mdsymi 10620  cdj3lem2 10644  elghom 10669  ghomgrpilem2 10671  ghomgrpi 10672  ghomgrplem 10674  ghomgrp 10675  ghomfo 10676  ghomlin 10678  ghomid 10679  ghomgsg 10680  ghomf1o 10682  symgoprv 10689  symggrpi 10691  symgidi 10692  cayleylem3 10696  cayleyi 10697  cayleyth 10699  tostos 10883  rngopid 10899  opidon2 10900  isexid2 10901  isppm 10917  seqzp2 10918  ismnd2 10928  grpmnd 10933  rnplrnml0 10946  rnplrnml 10948  rngdmdmrn 10949  rnplrnml3 10950  unmnd 10951  ununr 10955  uridm 10956  multinv 10959  multinvb 10960  mult2inv 10961  on1el3 10962  rngunval2 10965  ring1cl 10966  zrdivrng 10969  topindis 11009  cnrsfin 11012  cnrscoa 11013  mapdiscn 11014  nsn 11017  hmeocna 11025  hmeocnb 11026  cmphmp 11027  cnvhmpha 11031  cnvhmphb 11032  cnvhmph 11033  hmphsyma 11034  hmphre 11036  hmeogrp 11044  homcard 11045  top2ind 11050  subsp 11056  subtopsin2 11067  filesn 11072  filint 11075  fipfil2 11077  emnfil 11078  oefil2 11079  neifil 11080  filintf 11081  fgsb 11082  filint2 11084  fgsb2 11086  rcfpfil 11095  limfillem2 11102  dtopcl 11107  t2t1 11108  dtt2 11110  cnvtr 11161  doma 11182  coda 11183  ida 11184  cmppfa 11186  dcsda 11187  1ded 11192  dedalg 11197  idosd 11198  cmppfd 11199  domcmpd 11200  codcmpd 11201  rdmob 11202  rcmob 11203  aidm2 11204  dmrngcmp 11205  0ded 11211  0cat 11212  catded 11218  cmpasso 11227  cmpidb 11229  dmo 11230  cdmo 11231  jdmo 11232  cmpmorp 11233  morcat 11234  cmppfc1 11235  ishomd 11245  ehm 11246  dehm 11247  cehm 11248  mrdmcd 11249  eqidob 11250  homib 11251  hine 11252  cmphmia 11253  cmphmib 11254  iri 11255  cmpassoh 11256  homgrf 11257  imonclem 11268  ismonc 11269  idmon 11272  immon 11273  iepiclem 11278  isepic 11279  cinvlem2 11283  fmamo 11290  vidfunid 11291  iddvvidd 11292  idcvvidc 11293  fmp 11294  idfisf 11295  catsbc 11303  obsubc2 11304  idsubc 11305  domsubc 11306  codsubc 11307  subctct 11308  morsubc 11309  cmpsubc 11310  idsubidsup 11311  idsubfun 11312  dfiin2g 11400  fictblem 11422  fictb 11423  ordtype 11434  hartog 11436  onsdom 11437  omsublim 11448  opncldf2 11455  opnnei 11469  neiin 11470  hmeoclda 11475  subsubtop 11479  subcld 11480  subcls 11481  subntr 11482  cnsubsp 11483  cnsubsp2 11484  compsublem 11487  compsub 11488  cptclsscpt 11489  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  comptoppr 11495  alexsublem3 11498  dfcon2 11501  connsub 11502  cnconn 11503  conntoppr 11504  subtopmetlem 11505  subtopmet 11506  reconnlem4 11510  reconnlem5 11511  reconn 11512  ivthALT 11515  1stctop 11531  2ndc1stc 11538  fnessex 11545  fneuni 11546  refssex 11551  fneref 11554  refref 11555  fnetr 11556  reftr 11558  topfneec 11562  fnessref 11564  refssfne 11565  finptfin 11568  locfintop 11571  locfinnei 11573  lfinpfin 11574  locfincomp 11575  locfincf 11577  comppfsc 11578  neibastop2lem1 11580  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  topmtcl 11586  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  t0top 11601  t1top 11605  t1t0 11608  regtop 11610  isnrm2 11613  filfbas 11628  fgf 11632  fgss 11634  fbssfg 11635  fgid 11637  fgfil 11638  filrn 11643  neifg 11644  supfil 11645  isufil2 11650  ufilfil 11651  filssufillem 11655  filssufil 11656  ufileu 11658  filufint 11659  uffixfr 11660  fixufil 11661  ufinffr 11663  ufilen 11664  filcon 11665  fbaslim 11680  neiplim 11681  limfilcf 11683  flimcls 11684  hausfillim 11685  cnpfillim 11686  isfilmap 11689  elfilmap 11690  elfilmap3 11692  fmf 11693  fmbas 11694  filmapss 11696  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem4 11703  fmfnfm 11704  fmufil 11705  filfm 11706  sflimf 11708  isflimf 11709  flimfnei 11710  flimfcnp 11714  sfcls 11716  fclusbas 11722  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  uffclsflim 11728  fcluscnplem 11729  fcluscnp 11730  fcluscomplem 11732  fcluscomp 11733  ufcomp 11734  sfclusf 11736  isfclusf 11737  flfssfcf 11741  uffcfflf 11742  fclsfcnp 11743  reldir 11750  dirdm 11751  dirref 11752  dirtr 11753  dirge 11754  tosdir 11755  tailf 11756  istail 11757  tailmap 11759  filnetlem1 11763  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  gafo 11773  isga2 11774  ga0 11775  gaid 11776  ssga 11777  gagrp 11778  gaf 11779  gagrpid 11780  gaass 11781  gacan 11782  gapm 11784  f1elima 11818  upxp 11822  upixp 11823  findcard 11836  fimax 11837  sdclem1 11875  sdclem2 11876  sdc 11877  fsumltisumi 11886  isumshft2 11893  subspcld2 11902  subspabs 11903  neificl 11904  blssp 11908  metsstop 11909  stioo 11910  mettrifi2 11913  geomcau 11914  metdcn 11918  iitop 11932  iiuni 11933  iccst 11939  icoopnst 11940  iocopnst 11941  lincmb01cmp 11942  constcncf 11944  cncfco 11948  cnimass 11949  cnres 11950  cnres2 11951  cnresima 11952  cnss 11953  paste 11954  piececn 11955  cncfres 11956  hmeocn 11958  hmeocnv 11959  hmeoopn 11960  hmeocld 11961  tlmbr 11965  lmtlm 11969  tx1cn 11976  tx2cn 11977  uptx 11978  txcn 11979  txcnopab 11980  txcnoprab 11981  2txcn 11982  txsubsp 11983  txopn 11984  txcld 11985  totbndmet 11991  sstotbnd 11992  totbndss 11993  bndss 11998  blbnd 11999  totbndbnd 12000  ismtycnv 12005  ismtyhmeolem 12006  ismtyhmeo 12007  ismtybndlem 12008  ismtyres 12010  heiborlem1 12011  heiborlem18 12028  heiborlem23 12033  heiborlem33 12043  heiborlem40 12050  heiborlem42 12052  bfplem1 12054  bfplem2 12055  bfplem3 12056  bfplem8 12061  bfplem11 12064  bfp 12065  recms 12066  rrnval 12069  rrnmval 12070  rrndm 12071  rrnmet 12072  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  rrnheibor 12079  reheibor 12081  iccbnd 12082  icccmp 12083  iicmp 12084  phtpyval 12089  phtpyid 12091  phtpycom 12092  phtpycolem3 12095  phtpycolem4 12096  phtpycolem5 12097  isphtpc 12101  phtpcdm 12103  phtpcer 12104  hgrablkne0 12199  emhgrat 12201

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-cleq 1511

Copyright terms: Public domain