Theorem eqid 1473

Description: Class identity law (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41.

Assertion

Ref	Expression
eqid	⊢ A = A

Proof of Theorem eqid

Step	Hyp	Ref	Expression
1		pm4.2 170	. 2 ⊢ (x ∈ A ↔ x ∈ A)
2	1	eqriv 1472	1 ⊢ A = A

Syntax hints:   = wceq 954   ∈ wcel 956

This theorem is referenced by:  visset 1809  reu3 1927  sbcbii 1974  ssid 2076  uniiunlem 2128  dfnul2 2278  dfnul3 2279  noel 2280  npss0 2305  ifor 2377  snidg 2429  pri1 2446  snsspr 2466  int0 2542  syl5eqbr 2643  syl5eqbrr 2644  syl6breq 2649  ssbri 2652  opabbii 2666  so 2859  unisn2 2870  ralxfrALT 2895  nlim0 3022  ordun 3076  finds1 3154  relop 3270  ididg 3273  issetid 3275  dm0 3318  dmsn0 3319  dmsnsn0 3320  dmi 3321  xp11a 3469  xp11b 3470  funfn 3534  f0 3647  fnforn 3668  f1orn 3689  f1oabexg 3691  f1o00 3705  f1o0 3707  funbrfvb 3746  fnopabfv 3749  funfv 3761  fvco 3765  fvopab4g 3770  fvopab4gf 3772  fvreseq 3790  fvimacnvALT 3800  fopabco 3823  fopabcos 3824  fopabsn 3831  fconst2g 3836  funiunfv 3857  tfr1 3915  tfr2 3916  tfr3 3917  tz7.44-1 3919  rdglem1 3928  oprabbii 3988  oprabval2gf 4017  oprabval3 4021  oprabval6g 4023  1st2val 4085  2nd2val 4086  curry1 4088  curry1f 4089  curry1val 4090  df1st2 4116  df2nd2 4117  0lt1o 4137  oe0m 4147  oawordeu 4179  nneob 4245  ecelqsi 4282  ecoptocl 4293  ecopoprsym 4300  ecopoprtrn 4301  th3qlem2 4305  th3q 4307  en2d 4387  en2 4389  en3 4390  dom2d 4391  dom2 4392  pw2en 4432  sbth 4443  mapenlem2 4476  mapen 4477  mapxpen 4481  xpmapenlem4 4485  xpmapen 4487  unbnn 4527  unfilem3 4532  abfii3 4543  iunfi 4549  pwfi 4551  inf0 4586  inf3 4600  infeq5 4601  tz9.1 4626  tz9.12 4642  ssrankr1 4656  rankel 4660  rankpw 4664  r1rankid 4674  scott0 4697  cplem2 4701  aceq3 4713  aceq4 4714  aceq5 4720  aceq6a 4721  aceq6b 4722  ac6 4735  aceqkm 4761  numth 4764  weth 4767  zorn2lem6 4773  zornlem 4775  zorn2 4776  brdom7disj 4784  brdom6disj 4785  iundom 4792  cardsn 4814  unxpdomlem 4823  alephfp2 4881  dominf 4884  0npi 4990  recidpq 5051  0npr 5076  genpprecl 5084  00sr 5188  opelreal 5229  eqresr 5235  ltsor 5241  pncan3t 5357  leidt 5512  renfdisj 5520  ltpnft 5523  mnfltt 5524  mnfltpnf 5525  xrleidt 5541  divcan2 5693  nnleltp1t 5909  0nn0 6068  0z 6101  uzwo3 6174  zmin 6175  znq 6204  seq11 6262  seq1p1 6263  seq1fn 6265  seq1res 6272  shftfn 6288  shftvalt 6291  seq1shftid 6301  icoshftf1o 6352  seq1seqz 6481  seq1seq0 6485  seqzeq 6495  seqzres 6500  seqzres2 6501  dfseq0 6503  exp0t 6511  0expt 6529  sq0 6574  discrlem2 6595  discrlem 6597  sqrlem21 6631  sqrmsq 6647  replimt 6700  abs0 6822  fsum1 6951  fsump1 6952  fsumconst 6984  climsub 7074  climcmp 7082  caucvg2 7109  caucvg3 7111  iserzabs 7123  cvgcmp2 7125  cvgcmp2c 7127  cvgcmp3ce 7131  isumclim5t 7145  isumshft 7147  isumshft2 7148  isummulc1 7155  isummulc1ALT 7156  infcvgaux1 7162  infcvgaux2 7163  infcvg 7167  geolimi 7179  geolim 7180  geolim1i 7181  geolim1 7182  geosum 7184  geoisum 7185  geoisum1 7187  geoisum1c 7188  cvgratlem5 7197  cvgrat 7198  divccncf 7223  ivthlem8 7231  isupivth 7233  dsupivth 7235  ivthlem8OLD 7240  ivthOLD 7241  efseq1ex 7256  dfef2 7257  efclt 7262  efcvgfsum 7265  reefcl 7267  erelem2 7270  erelem6 7274  ereALT 7281  ege2 7282  ele3 7283  ege2le3 7284  ef0 7285  efcj 7286  efaddlem23 7310  efaddlem27 7314  efaddlem28 7315  efadd 7316  eftlext 7328  ef1tlub 7332  ef01tllem2 7334  ef01tlub 7335  absef01tlub 7337  eirrlem3 7340  eirr 7343  ef4p 7348  ef4pt 7349  efge1 7350  efge1p 7351  absefm1le 7360  eflegeo 7363  efcnlem3 7369  reeff1olem2 7373  reeff1olem2OLD 7375  sin01bndlem2 7418  cos01bndlem2 7420  sin01bnd 7422  cos01bnd 7423  acdc3lem 7436  acdc3 7437  acdc2lem2 7439  acdc2 7440  acdc5lem2 7442  acdc5 7443  acdclem 7444  acdc 7445  acdcALT 7446  nnenom 7448  qnnen 7454  unben 7456  infpn 7459  ruclem15 7475  ruclem38 7498  infxpidmlem9 7511  infxpidm 7515  infmap2 7531  eltopsp 7554  tpsex 7555  istps2 7557  basgen2t 7589  ntrval 7626  clsval 7627  0cld 7628  iincld 7629  uncld 7631  cldcls 7632  cls0 7659  ntr0 7660  neival 7667  neii2 7672  neiss 7673  opnneiss 7682  innei 7686  neissex 7688  lpval 7693  qdensere 7701  cnpval 7709  cnpimaex 7715  cnima 7717  cnco 7718  cnpco 7719  cnclima 7721  haustop 7736  dfms2 7749  met0 7765  metres 7775  metxpcl 7784  metxplem4 7785  metxp 7786  blfval 7787  blval 7789  blrn 7793  blf 7796  blelrn 7800  blss 7805  opni 7816  opni2 7817  opni3 7818  blssopn 7819  opnuni 7820  opnin 7821  unirnbl 7827  neibl 7829  lpbl 7832  methausi 7833  methaus 7834  metcnpf 7835  metcnf 7836  metcnconst 7837  metcnp 7839  metcn 7841  metcnss 7850  metcnss2 7851  metidcn 7852  metdnsconst 7853  cncfmet 7857  remetdval 7860  remet 7862  tgioo 7867  rehaus 7869  lmrel 7879  lmbr 7880  lmuni 7902  lmsslem 7903  lmss 7904  caussi 7905  causs 7906  lmfex 7910  cmsmet 7912  metelcls 7916  metcld 7917  metcn4 7921  metcn4i 7922  oprcn 7927  opr1cn 7928  opr2cn 7929  opr1scn 7930  addcn 7936  subcn 7937  mulcn 7938  fsumcnlem 7939  fsumcn 7940  iscms2 7944  lmcau 7946  cmsss 7947  bcthlem32 7980  bcth 7982  grprndm 8004  0ngrp 8005  grprn 8006  grprcan 8013  grpinvval 8017  grpinvcl 8018  grpinvid 8024  grplcan 8025  grpasscan1 8027  grp2inv 8028  grpinvf 8029  grpinvop 8030  grpdivfval 8031  grpdivval 8032  grpdivf 8035  grpdivdiv 8037  grpmuldivass 8038  grpdivid 8039  grppncan 8040  grpnpcan 8041  grppnpcan2 8042  grpnnncan2 8043  resgrprn 8045  resgrprnOLD 8046  grplactval 8048  grplactf1o 8049  ablgrp 8053  abldivdiv4 8061  ablnncan 8064  subgres 8069  subgid 8072  subgabl 8075  cnid 8079  addinv 8080  readdsubg 8081  zaddsubg 8082  mulid 8084  ghgrpi 8089  ringabl 8102  vcabl 8128  vcm 8142  vcrinv 8143  vclinv 8144  vcoprnelem 8149  vcoprne 8150  vcex 8151  cnvc 8154  nvvop 8180  nvex 8182  nvvc 8186  nvabl 8187  nvsf 8190  nvscl 8199  nvsid 8200  nvsass 8201  nvdi 8203  nvdir 8204  nv2 8205  vsfval 8206  nvzcl 8207  nv0 8210  nvsz 8211  nvinv 8212  invfval 8213  nvmval 8215  nvmfval 8216  nvzs 8217  nvmf 8218  nvnnncan1 8220  nvnnncan2 8221  nvmdi 8222  nvnegneg 8223  nvrinv 8225  nvlinv 8226  nvsubadd 8227  nvpncan2 8228  nvaddsub4 8233  nvsubsub23 8234  nvnncan 8235  nvmeq0 8236  nvmid 8237  nvf 8238  nvdm 8241  nvs 8242  nvsub 8247  nvz0 8248  nvz 8249  nvtri 8250  nvmtri 8251  nvmtri2 8252  nvabs 8253  nvge0 8254  nvop 8257  cnnvg 8259  cnnvba 8260  cnnvdemo 8261  cnnvs 8262  cnnvnm 8263  cnnvm 8264  elimnvu 8266  imsdval2 8269  nvnd 8270  imsdf 8271  imsmet 8275  nvelbl 8276  nvelbl2 8277  nvcnf 8278  nvcni 8279  nvlmcl 8280  nvlmle 8281  cnims 8282  sqcn 8283  sqcn2 8284  nmcni 8286  nmcn 8287  nmcn2 8288  nmcnc 8289  abscn 8290  abscncfALT 8291  va1cnlem 8292  va1cn 8293  sm1cnilem 8294  sm1cni 8295  ipfval 8299  ipval 8300  ipid 8310  ipcl 8312  ipf 8313  ipcj 8314  ip0r 8317  ipz 8319  ip1cnilem2 8321  ip1cnilem3 8322  ip1cnilem4 8323  ip1cnilem5 8324  ip1cni 8326  sspval 8329  sspid 8331  sspnv 8332  sspba 8333  sspg 8334  ssps 8336  sspmlem 8338  sspmval 8339  sspm 8340  sspz 8341  sspn 8342  sspival 8344  sspi 8345  sspimsval 8346  sspims 8347  lnoval 8360  lnof 8363  lno0 8364  lnocoi 8365  lnosub 8366  lnomul 8367  nvcnpi4 8368  nvo00 8369  nmoval 8371  nmosetn0 8373  nmoxr 8374  nmoge0 8375  nmorepnf 8376  nmolb 8379  isblo2 8388  bloln 8389  blof 8390  nmblore 8391  0oo 8394  0lno 8395  nmo0 8396  0blo 8397  nmlno0lem 8398  nmlno0i 8399  nmlno0 8400  nmlnoubi 8401  nmlnogt0 8402  nmblolbii 8403  nmblolbi 8404  isblo3i 8405  blometi 8407  blocnilem 8408  blocni 8409  blocn 8411  blocn2 8412  phop 8421  cnph 8422  elimphu 8424  isph 8425  ip0i 8428  ip1i 8430  ip2i 8431  ipdirilem 8432  ipdiri 8433  ipasslem1 8434  ipasslem2 8435  ipasslem6 8439  ipasslem7 8440  ipasslem8 8441  ipasslem9 8442  ipasslem11 8444  ipassi 8445  ipdir 8446  ipass 8449  ipsubdir 8452  siii 8457  sii 8458  sspph 8459  ipblnfi 8460  ip2eqi 8461  phoeqi 8462  ajfuni 8464  ajfun 8465  bnnv 8470  cnbn 8472  ubthlem3 8475  ubthlem4 8476  ubthlem6 8478  ubthlem9 8481  ubthlem11 8483  ubthlem12 8484  ubthlem13 8485  ubthlem14 8486  ubthii 8487  ubthi 8488  minveclem1 8489  minveclem2 8490  minveclem3 8491  minveclem9 8497  minveclem16 8504  minveclem21 8509  minveclem23 8511  minveclem28 8516  minveclem29 8517  minveclem33 8521  minvecex 8522  minveclem37 8525  minveceu 8527  minvecex2 8532  hlipgt0 8559  hlcompl 8560  htthlem4 8566  htthlem5 8567  htthlem12 8574  htthi 8575  pstr 8594  spwval2 8595  spwval 8600  spwnex 8602  sincnlem 8604  sinco 8605  cosco 8606  sincn 8607  coscn 8608  pilem2 8610  pilem3 8611  pilem4 8612  efghgrpilem 8653  efghgrpi 8654  efifolem1 8656  efifolem4 8659  shftefif1olem 8680  shftefif1o 8681  eff1oi 8685  eff1o 8687  h2hva 8782  h2hsm 8783  h2hnm 8784  h2hvs 8785  axhcompl 8807  hiidrclt 8900  normlem7 8921  norm-ii 8943  hilid 8967  hilvc 8968  hilnorm 8969  hhba 8973  hh0v 8974  hhims 8978  hhims2 8979  hhip 8983  hhph 8984  bcsHIL 8986  hilmet 9000  hilmetdval 9001  hilmetba 9002  hhhl 9012  hilcms 9013  hilhl 9014  hhssva 9068  hhsssm 9069  hhssnm 9070  hhssabl 9071  hhssnv 9073  hhssnvt 9074  hhsst 9075  hhshsslem1 9076  hhshsslem2 9077  hhsssh 9078  hhsssh2 9079  hhssba 9080  hhssvs 9081  hhssph 9083  hhssims 9084  hhssims2 9085  hhssbn 9090  occllem7 9118  projlem8 9132  projlem10 9134  projlem31 9155  projlem 9156  pjthlem13 9169  pjth 9171  pjvalt 9177  shsvat 9222  hosvalt 9456  hosvaltOLD 9457  homvalt 9458  hodvalt 9459  hodvaltOLD 9460  hfsvalt 9461  hfmvalt 9462  pjcomp 9559  dfiop2 9619  hoaddclt 9624  homulclt 9625  hoeqt 9626  hodseq 9660  ho01 9694  hoeq1t 9696  nmopsetretHIL 9731  nmopsetn0 9732  nmfnsetn0 9745  hhlno 9766  hhblo 9768  hh0o 9769  nmoplbt 9771  nmfnlbt 9787  bravalvalt 9807  brafnt 9810  kbopt 9816  kbvalvalt 9817  kbpjt 9819  eigvalt 9823  hmopbdopHIL 9851  nmlnop0ALT 9858  nmlnop0HIL 9859  lnopco0 9867  nmcopex 9895  lnopcon 9901  nmcfnex 9924  lnfncon 9928  cnlnadj 9947  nmopadjle 9959  kbass2t 9988  kbass5t 9991  leopsqt 10000  hmopidmpj 10018  hmopidmcht 10019  hmopidmpjt 10020  pjssdif2 10040  pjinvar 10057  str 10122  hstr 10130  goeq 10138  irred 10258  mdsymlem8 10274  mdsym 10275  cdj3lem2 10296  elghom 10318  ghomgrpilem2 10320  ghomgrpi 10321  ghomgrplem 10323  ghomgrp 10324  ghomfo 10325  ghomlin 10327  ghomid 10328  ghomgsg 10329  ghomf1o 10331  symgoprval 10338  symggrpi 10340  symgidi 10341  cayleylem2 10344  cayleylem3 10345  cayleyi 10346  cayleyth 10348  cnrsfin 10432  cnrscoa 10433  mapdiscn 10434  hmeocna 10442  hmeocnb 10443  cmphmp 10444  cnvhmpha 10448  cnvhmphb 10449  cnvhmph 10450  hmphsyma 10451  hmphre 10453  hmeogrp 10461  homcard 10462  subsp 10465  filesn 10470  filint 10473  fipfil2 10475  emnfil 10476  oefil2 10477  neifil 10478  filintf 10479  fgsb 10480  filint2 10482  fgsb2 10485  dtopcl 10495  t2t1 10496  dtt2 10498  cnvtr 10518  doma 10541  coda 10542  ida 10543  cmppfa 10545  dcsda 10546  1ded 10551  dedalg 10556  idosd 10557  cmppfd 10558  domcmpd 10559  codcmpd 10560  rdmob 10561  rcmob 10562  aidm 10563  aidmold 10564  0ded 10570  0cat 10571  catded 10577  cmpasso 10586  cmpidb 10588  dmo 10589  cdmo 10590  jdmo 10591  cmpmorp 10592  ishomd 10598  ehm 10599  dehm 10600  cehm 10601  mrdmcd 10602  eqidob 10603  homib 10604  hine 10605  cmphmia 10606  cmphmib 10607  iri 10608  cmpassoh 10609  homgrf 10610  imonclem 10619  ismonc 10620  idmon 10624  immon 10625  fmamo 10630  vidfunid 10631  iddvvidd 10632  idcvvidc 10633  hgrablkne0 10645  emhgrat 10647

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

This theorem depends on definitions:  df-bi 147  df-cleq 1467

Copyright terms: Public domain