Theorem eqid 1468

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 e. A <-> x e. A)
2	1	eqriv 1467	1 |- A = A

Syntax hints:   = wceq 953   e. wcel 955

This theorem is referenced by:  visset 1804  reu3 1921  sbcbii 1968  ssid 2070  uniiunlem 2122  dfnul2 2272  dfnul3 2273  noel 2274  npss0 2299  ifor 2371  snidg 2423  pri1gOLD 2440  pri1 2441  snsspr 2461  int0 2537  syl5eqbr 2638  syl5eqbrr 2639  syl6breq 2644  ssbri 2647  opabbii 2661  so 2855  unisn2 2866  ralxfrALT 2890  nlim0 3017  ordun 3071  finds1 3149  relop 3265  ididg 3268  issetid 3269  dm0 3312  dmsn0 3313  dmsnsn0 3314  dmi 3315  xp11a 3464  funfn 3528  f0 3641  fnforn 3662  f1orn 3683  f1oabexg 3685  f1o00 3699  f1o0 3701  funbrfvb 3740  fnopabfv 3743  funfv 3755  fvco 3759  fvopab4g 3764  fvopab4gf 3766  fvreseq 3784  fvimacnvALT 3794  fopabco 3817  fopabcos 3818  fopabsn 3825  fconst2g 3830  funiunfv 3851  tfr1 3909  tfr2 3910  tfr3 3911  tz7.44-1 3913  rdglem1 3922  oprabbii 3982  oprabval2gf 4011  oprabval3 4015  oprabval6g 4017  1st2val 4079  2nd2val 4080  curry1 4082  curry1f 4083  curry1val 4084  df1st2 4110  df2nd2 4111  0lt1o 4131  oe0m 4141  oawordeu 4173  nneob 4239  ecelqsi 4276  ecoptocl 4287  ecopoprsym 4294  ecopoprtrn 4295  th3qlem2 4299  th3q 4301  en2d 4381  en2 4383  en3 4384  dom2d 4385  dom2 4386  pw2en 4426  sbth 4437  mapenlem2 4470  mapen 4471  mapxpen 4475  xpmapenlem4 4479  xpmapen 4481  unbnn 4521  unfilem3 4526  abfii3 4537  iunfi 4543  pwfi 4545  inf0 4578  inf3 4592  infeq5 4593  tz9.1 4618  tz9.12 4634  ssrankr1 4648  rankel 4652  rankpw 4656  r1rankid 4666  scott0 4689  cplem2 4693  aceq3 4705  aceq4 4706  aceq5 4712  aceq6a 4713  aceq6b 4714  ac6 4727  aceqkm 4753  numth 4756  weth 4759  zorn2lem6 4765  zornlem 4767  zorn2 4768  brdom7disj 4776  brdom6disj 4777  iundom 4784  cardsn 4806  unxpdomlem 4815  alephfp2 4873  dominf 4876  0npi 4982  recidpq 5043  0npr 5068  genpprecl 5076  00sr 5180  opelreal 5221  eqresr 5227  ltsor 5233  pncan3t 5349  leidt 5504  renfdisj 5512  ltpnft 5515  mnfltt 5516  mnfltpnf 5517  xrleidt 5533  divcan2 5685  nnleltp1t 5901  0nn0 6060  0z 6093  uzwo3 6166  zmin 6167  znq 6196  seq11 6254  seq1p1 6255  seq1fn 6257  seq1res 6264  shftfn 6280  shftvalt 6283  seq1shftid 6293  icoshftf1o 6344  seq1seqz 6473  seq1seq0 6477  seqzeq 6487  seqzres 6492  seqzres2 6493  dfseq0 6495  exp0t 6503  0expt 6521  sq0 6566  discrlem2 6587  discrlem 6589  sqrlem21 6623  sqrmsq 6639  replimt 6692  abs0 6814  fsum1 6943  fsump1 6944  fsumconst 6976  climsub 7066  climcmp 7074  caucvg2 7101  caucvg3 7103  iserzabs 7115  cvgcmp2 7117  cvgcmp2c 7119  cvgcmp3ce 7123  isumclim5t 7137  isumshft 7139  isumshft2 7140  isummulc1 7147  isummulc1ALT 7148  infcvgaux1 7154  infcvgaux2 7155  infcvg 7159  geolimi 7171  geolim 7172  geolim1i 7173  geolim1 7174  geosum 7176  geoisum 7177  geoisum1 7179  geoisum1c 7180  cvgratlem5 7189  cvgrat 7190  divccncf 7215  ivthlem8 7223  isupivth 7225  dsupivth 7227  ivthlem8OLD 7232  ivthOLD 7233  efseq1ex 7248  dfef2 7249  efclt 7254  efcvgfsum 7257  reefcl 7259  erelem2 7262  erelem6 7266  ereALT 7273  ege2 7274  ele3 7275  ege2le3 7276  ef0 7277  efcj 7278  efaddlem23 7302  efaddlem27 7306  efaddlem28 7307  efadd 7308  eftlext 7320  ef1tlub 7324  ef01tllem2 7326  ef01tlub 7327  absef01tlub 7329  eirrlem3 7332  eirr 7335  ef4p 7340  ef4pt 7341  efge1 7342  efge1p 7343  absefm1le 7352  eflegeo 7355  efcnlem3 7361  reeff1olem2 7365  reeff1olem2OLD 7367  sin01bndlem2 7410  cos01bndlem2 7412  sin01bnd 7414  cos01bnd 7415  acdc3lem 7428  acdc3 7429  acdc2lem2 7431  acdc2 7432  acdc5lem2 7434  acdc5 7435  acdclem 7436  acdc 7437  acdcALT 7438  nnenom 7440  qnnen 7446  unben 7448  infpn 7451  ruclem15 7467  ruclem38 7490  infxpidmlem9 7503  infxpidm 7507  infmap2 7523  eltopsp 7546  tpsex 7547  istps2 7549  basgen2t 7581  ntrval 7618  clsval 7619  0cld 7620  iincld 7621  uncld 7623  cldcls 7624  cls0 7651  neival 7658  neii2 7663  neiss 7664  opnneiss 7673  innei 7677  neissex 7679  lpval 7684  qdensere 7691  cnpval 7699  cnpimaex 7704  cnima 7706  cnco 7707  cnpco 7708  cnclima 7710  haustop 7725  dfms2 7738  met0 7754  metres 7763  metxpcl 7772  metxplem4 7773  metxp 7774  blfval 7775  blval 7777  blrn 7781  blf 7784  blelrn 7788  blss 7793  opni 7804  opni2 7805  opni3 7806  blssopn 7807  opnuni 7808  opnin 7809  unirnbl 7815  neibl 7817  lpbl 7819  methausi 7820  methaus 7821  metcnpf 7822  metcnf 7823  metcnconst 7824  metcnp 7826  metcn 7828  metcnss 7837  metcnss2 7838  metidcn 7839  metdnsconst 7840  cncfmet 7844  remetdval 7847  remet 7849  tgioo 7854  lmrel 7865  lmbr 7866  lmuni 7886  lmsslem 7887  lmss 7888  caussi 7889  causs 7890  lmfex 7894  cmsmet 7896  metelcls 7900  metcld 7901  metcn4 7905  metcn4i 7906  oprcn 7911  opr1cn 7912  opr2cn 7913  opr1scn 7914  addcn 7920  subcn 7921  mulcn 7922  fsumcnlem 7923  fsumcn 7924  iscms2 7928  lmcau 7930  cmsss 7931  bcthlem32 7964  bcth 7966  grprndm 7988  0ngrp 7989  grprn 7990  grprcan 7997  grpinvval 8001  grpinvcl 8002  grpinvid 8009  grplcan 8010  grpasscan1 8012  grp2inv 8013  grpinvf 8014  grpinvop 8015  grpdivfval 8016  grpdivval 8017  grpdivf 8020  grpdivdiv 8022  grpmuldivass 8023  grpdivid 8024  grppncan 8025  grpnpcan 8026  grppnpcan2 8027  grpnnncan2 8028  resgrprn 8030  resgrprnOLD 8031  grplactval 8033  grplactf1o 8034  ablgrp 8038  abldivdiv4 8046  ablnncan 8049  subgres 8054  subgid 8057  subgabl 8060  cnid 8064  addinv 8065  readdsubg 8066  zaddsubg 8067  mulid 8069  ghgrpi 8074  ringabl 8087  vcabl 8113  vcm 8127  vcrinv 8128  vclinv 8129  vcoprnelem 8135  vcoprne 8136  vcex 8137  cnvc 8140  nvvop 8166  nvex 8169  nvvc 8174  nvabl 8175  nvsf 8178  nvscl 8187  nvsid 8188  nvsass 8189  nvdi 8191  nvdir 8192  nv2 8193  vsfval 8194  nvzcl 8195  nv0 8198  nvsz 8199  nvinv 8200  invfval 8201  nvmval 8203  nvmfval 8204  nvzs 8205  nvmf 8206  nvnnncan1 8208  nvnnncan2 8209  nvmdi 8210  nvnegneg 8211  nvrinv 8213  nvlinv 8214  nvsubadd 8215  nvpncan2 8216  nvaddsub4 8221  nvsubsub23 8222  nvnncan 8223  nvmeq0 8224  nvmid 8225  nvf 8226  nvs 8229  nvsub 8234  nvz0 8235  nvz 8236  nvtri 8237  nvmtri 8238  nvmtri2 8239  nvabs 8240  nvge0 8241  nvop 8244  cnnvg 8246  cnnvba 8247  cnnvdemo 8248  cnnvs 8249  cnnvnm 8250  cnnvm 8251  elimnvu 8253  imsdval2 8256  nvnd 8257  imsdf 8258  imsmet 8262  nvelbl 8263  nvelbl2 8264  nvcnf 8265  nvcni 8266  nvlmcl 8267  nvlmle 8268  cnims 8269  sqcn 8270  sqcn2 8271  nmcni 8273  nmcn 8274  nmcn2 8275  nmcnc 8276  abscn 8277  abscncfALT 8278  va1cnlem 8279  va1cn 8280  sm1cnilem 8281  sm1cni 8282  ipfval 8286  ipval 8287  ipid 8297  ipcl 8299  ipf 8300  ipcj 8301  ip0r 8304  ipz 8306  ip1cnilem2 8308  ip1cnilem3 8309  ip1cnilem4 8310  ip1cnilem5 8311  ip1cni 8313  sspval 8316  sspid 8318  sspnv 8319  sspba 8320  sspg 8321  ssps 8323  sspmlem 8325  sspmval 8326  sspm 8327  sspz 8328  sspn 8329  sspival 8331  sspi 8332  sspimsval 8333  sspims 8334  lnoval 8347  lnof 8350  lno0 8351  lnocoi 8352  lnosub 8353  lnomul 8354  nvcnpi4 8355  nvo00 8356  nmoval 8358  nmosetn0 8360  nmoxr 8361  nmoge0 8362  nmorepnf 8363  nmolb 8366  isblo2 8375  bloln 8376  blof 8377  nmblore 8378  0oo 8381  0lno 8382  nmo0 8383  0blo 8384  nmlno0lem 8385  nmlno0i 8386  nmlno0 8387  nmlnoubi 8388  nmlnogt0 8389  nmblolbii 8390  nmblolbi 8391  isblo3i 8392  blometi 8394  blocnilem 8395  blocni 8396  blocn 8398  blocn2 8399  phop 8408  cnph 8409  elimphu 8411  isph 8412  ip0i 8415  ip1i 8417  ip2i 8418  ipdirilem 8419  ipdiri 8420  ipasslem1 8421  ipasslem2 8422  ipasslem6 8426  ipasslem7 8427  ipasslem8 8428  ipasslem9 8429  ipasslem11 8431  ipassi 8432  ipdir 8433  ipass 8436  ipsubdir 8439  siii 8444  sii 8445  sspph 8446  ipblnfi 8447  ip2eqi 8448  phoeqi 8449  ajfuni 8451  ajfun 8452  bnnv 8457  cnbn 8459  ubthlem3 8462  ubthlem4 8463  ubthlem6 8465  ubthlem9 8468  ubthlem11 8470  ubthlem12 8471  ubthlem13 8472  ubthlem14 8473  ubthii 8474  ubthi 8475  minveclem1 8476  minveclem2 8477  minveclem3 8478  minveclem9 8484  minveclem16 8491  minveclem21 8496  minveclem23 8498  minveclem28 8503  minveclem29 8504  minveclem33 8508  minvecex 8509  minveclem37 8512  minveceu 8514  minvecex2 8519  hlipgt0 8546  hlcompl 8547  htthlem4 8553  htthlem5 8554  htthlem12 8561  htthi 8562  spwval2 8577  spwval 8582  sincnlem 8585  sinco 8586  cosco 8587  sincn 8588  coscn 8589  pilem2 8591  pilem3 8592  pilem4 8593  efghgrpilem 8634  efghgrpi 8635  efifolem1 8637  efifolem4 8640  shftefif1olem 8661  shftefif1olemOLD 8662  shftefif1o 8663  eff1oi 8668  eff1o 8670  h2hva 8782  h2hsm 8783  h2hnm 8784  h2hvs 8785  hiidrclt 8882  normlem7 8903  norm-ii 8925  hilid 8949  hilvc 8950  hilnorm 8951  hhba 8955  hh0v 8956  hhims 8960  hhims2 8961  hhip 8965  hhph 8966  bcsHIL 8968  hilmet 8982  hilmetdval 8983  hilmetba 8984  hhhl 8994  hilcms 8995  hilhl 8996  hhssva 9050  hhsssm 9051  hhssnm 9052  hhssabl 9053  hhssnv 9054  hhssnvt 9055  hhsst 9056  hhshsslem1 9057  hhshsslem2 9058  hhsssh 9059  hhssba 9060  hhssvs 9061  hhssph 9063  hhssbn 9068  occllem7 9095  projlem8 9109  projlem10 9111  projlem31 9132  projlem 9133  pjthlem13 9146  pjth 9148  pjvalt 9154  shsvat 9199  hosvalt 9433  hosvaltOLD 9434  homvalt 9435  hodvalt 9436  hodvaltOLD 9437  hfsvalt 9438  hfmvalt 9439  pjcomp 9536  dfiop2 9596  hoaddclt 9601  homulclt 9602  hoeqt 9603  hodseq 9637  ho01 9671  hoeq1t 9673  nmopsetretHIL 9708  nmopsetn0 9709  nmfnsetn0 9722  hhlno 9743  hhblo 9745  hh0o 9746  nmoplbt 9748  nmfnlbt 9764  bravalvalt 9784  brafnt 9787  kbopt 9793  kbvalvalt 9794  kbpjt 9796  eigvalt 9800  hmopbdopHIL 9828  nmlnop0ALT 9835  nmlnop0HIL 9836  lnopco0 9844  nmcopex 9872  lnopcon 9878  nmcfnex 9901  lnfncon 9905  cnlnadj 9924  nmopadjle 9936  kbass2t 9962  kbass5t 9965  leopsqt 9974  hmopidmpj 9991  hmopidmcht 9992  hmopidmpjt 9993  pjssdif2 10013  pjinvar 10029  str 10094  hstr 10102  goeq 10110  irred 10229  mdsymlem8 10245  mdsym 10246  cdj3lem2 10267  elghom 10289  ghomgrpilem2 10291  ghomgrpi 10292  ghomgrplem 10294  ghomgrp 10295  ghomfo 10296  ghomlin 10298  ghomid 10299  ghomgsg 10300  ghomf1o 10302  symgoprval 10309  symgidiOLD 10312  symggrpi 10313  symgidi 10314  cayleylem2 10317  cayleylem3 10318  cayleyi 10319  cayleyth 10321  cnrsfin 10396  cnrscoa 10397  mapdiscn 10398  hmeocna 10406  hmeocnb 10407  cmphmp 10408  cnvhmpha 10412  cnvhmphb 10413  cnvhmph 10414  hmphsyma 10415  hmphre 10417  hmeogrp 10425  homcard 10426  subsp 10429  filesn 10434  filint 10437  fipfil2 10439  emnfil 10440  oefil2 10441  neifil 10442  filintf 10443  fgsb 10444  filint2 10446  fgsb2 10449  dtopcl 10459  t2t1 10460  dtt2 10462  cnvtr 10482  doma 10505  coda 10506  ida 10507  cmppfa 10509  dcsda 10510  1ded 10515  dedalg 10520  idosd 10521  cmppfd 10522  domcmpd 10523  codcmpd 10524  rdmob 10525  rcmob 10526  aidm 10527  aidmold 10528  0ded 10534  0cat 10535  catded 10541  cmpasso 10550  cmpidb 10552  dmo 10553  cdmo 10554  jdmo 10555  cmpmorp 10556  ishomd 10562  ehm 10563  dehm 10564  cehm 10565  mrdmcd 10566  eqidob 10567  homib 10568  hine 10569  cmphmia 10570  cmphmib 10571  iri 10572  cmpassoh 10573  homgrf 10574  imonclem 10583  ismonc 10584  idmon 10588  immon 10589  fmamo 10594  vidfunid 10595  iddvvidd 10596  idcvvidc 10597  hgrablkne0 10609  emhgrat 10611

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

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

Copyright terms: Public domain