Theorem eqid 1478

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 1477	1 |- A = A

Syntax hints:   = wceq 958   e. wcel 960

This theorem is referenced by:  eqidd 1479  visset 1816  reu3 1934  sbcbii 1982  ssid 2084  uniiunlem 2136  dfnul2 2286  dfnul3 2287  noel 2288  npss0 2314  ifor 2386  snidg 2438  pri1 2455  snsspr 2475  int0 2552  syl5eqbr 2654  syl5eqbrr 2655  syl6breq 2660  ssbri 2663  opabbii 2677  so 2871  unisn2 2882  ralxfrALT 2907  nlim0 3034  ordun 3088  finds1 3166  relop 3282  ididg 3285  issetid 3287  dm0 3330  dmsn0 3331  dmsnsn0 3332  dmi 3333  xp11a 3484  xp11b 3485  funfn 3549  f0 3663  fnforn 3684  f1orn 3705  f1oabexg 3707  f1o00 3721  f1o0 3723  funbrfvb 3762  fnopabfv 3765  funfv 3777  fvco 3781  fvopab4g 3786  fvopab4gf 3788  fvreseq 3806  fvimacnvALT 3816  fopabco 3839  fopabcos 3840  fopabsn 3847  fconst2g 3852  funiunfv 3873  tfr1 3931  tfr2 3932  tfr3 3933  tz7.44-1 3935  rdglem1 3944  oprabbii 4004  oprabval2gf 4033  oprabval3 4037  oprabval6g 4039  1st2val 4102  2nd2val 4103  curry1 4105  curry1f 4106  curry1val 4107  df1st2 4133  df2nd2 4134  0lt1o 4154  oe0m 4164  oawordeu 4196  nneob 4262  ecelqsi 4299  ecoptocl 4310  ecopoprsym 4317  ecopoprtrn 4318  th3qlem2 4322  th3q 4324  en2d 4407  en2 4409  en3 4410  dom2d 4411  dom2 4412  pw2en 4453  sbth 4464  mapenlem2 4497  mapen 4498  mapxpen 4502  xpmapenlem4 4506  xpmapen 4508  unbnn 4557  unfilem3 4564  abfii3 4581  pwfi 4586  pwfiOLD 4587  inf0 4622  inf3 4636  infeq5 4637  tz9.1 4663  tz9.12 4679  ssrankr1 4693  rankel 4697  rankpw 4701  r1rankid 4711  scott0 4734  cplem2 4738  aceq3 4750  aceq4 4751  aceq5 4757  aceq6a 4758  aceq6b 4759  ac6 4772  aceqkm 4798  numth 4801  weth 4804  zorn2lem6 4810  zornlem 4812  zorn2 4813  brdom7disj 4821  brdom6disj 4822  iundom 4829  cardsn 4851  unxpdomlem 4861  alephfp2 4919  dominf 4922  dominfOLD 4923  0npi 5029  recidpq 5090  0npr 5115  genpprecl 5123  00sr 5227  opelreal 5268  eqresr 5274  ltsor 5280  pncan3t 5396  leidt 5550  renfdisj 5558  ltpnft 5561  mnfltt 5562  mnfltpnf 5563  xrleidt 5579  divcan2 5735  nnleltp1t 5963  0nn0 6122  0z 6155  uzwo3 6227  zmin 6228  fldivt 6263  znq 6266  seq11 6325  seq1p1 6326  seq1fn 6328  seq1res 6335  shftfn 6351  shftvalt 6354  seq1shftid 6364  icoshftf1o 6419  seq1seqz 6549  seq1seq0 6553  seqzeq 6563  seqzres 6568  seqzres2 6569  dfseq0 6571  exp0t 6579  0expt 6598  sq0 6643  discrlem2 6665  discrlem 6667  sqrlem21 6701  sqrmsq 6717  replimt 6769  abs0 6884  fsum1 7012  fsump1 7013  climsub 7137  climcmp 7145  caucvg2 7172  caucvg3 7174  iserzabs 7186  cvgcmp2 7188  cvgcmp2c 7190  cvgcmp3ce 7194  isumclim5t 7209  isumshft 7211  isumshft2 7212  isummulc1 7219  isummulc1ALT 7220  infcvgaux1 7226  infcvgaux2 7227  infcvg 7231  geolimi 7243  geolim 7244  geolim1i 7245  geolim1 7246  geosum 7248  geoisum 7249  geoisum1 7251  geoisum1c 7252  cvgratlem5 7261  cvgrat 7262  divccncf 7287  ivthlem8 7295  isupivth 7297  dsupivth 7299  efseq1ex 7313  dfef2 7314  efclt 7319  efcvgfsum 7322  reefcl 7324  erelem2 7327  erelem6 7331  ereALT 7338  ege2 7339  ele3 7340  ege2le3 7341  ef0 7342  efcj 7343  efaddlem23 7367  efaddlem27 7371  efaddlem28 7372  efadd 7373  eftlext 7385  ef1tlub 7389  ef01tllem2 7391  ef01tllem2OLD 7392  ef01tlub 7393  absef01tlub 7395  eirrlem3 7398  eirr 7401  ef4p 7406  ef4pt 7407  efge1 7408  efge1p 7409  absefm1le 7419  eflegeo 7422  efcnlem3 7428  reeff1olem2 7432  sin01bndlem2 7476  cos01bndlem2 7478  sin01bnd 7480  cos01bnd 7481  acdc3 7495  acdc2lem2 7497  acdc2 7498  acdc5lem2 7500  acdc5 7501  acdc 7503  acdcALT 7504  nnenom 7506  qnnen 7511  unben 7513  infpn 7516  ruclem15 7532  ruclem38 7555  infxpidmlem9 7568  infxpidm 7572  infmap2 7590  eltopsp 7612  tpsex 7613  istps2 7615  basgen2t 7645  ntrval 7680  clsval 7681  0cld 7682  iincld 7683  uncld 7685  cldcls 7686  cls0 7713  ntr0 7714  neival 7721  neii2 7726  neiss 7727  opnneiss 7736  innei 7740  neissex 7742  lpval 7747  qdensere 7755  cnpval 7763  cnpimaex 7769  cnima 7771  cnco 7772  cnpco 7773  cnclima 7775  haustop 7790  dfms2 7803  met0 7819  metres 7827  metxpcl 7836  metxplem4 7837  metxp 7838  blfval 7839  blval 7841  blrn 7845  blf 7848  blelrn 7852  blss 7857  opni 7868  opni2 7869  opni3 7870  blssopn 7871  opnuni 7872  opnin 7873  unirnbl 7879  neibl 7881  lpbl 7884  methausi 7885  methaus 7886  metcnpf 7887  metcnf 7888  metcnconst 7889  metcnp 7891  metcn 7893  metcnss 7902  metcnss2 7903  metidcn 7904  metdnsconst 7905  cncfmet 7909  remetdval 7912  remet 7914  tgioo 7919  rehaus 7921  lmrel 7931  lmbr 7932  lmuni 7955  lmsslem 7956  lmss 7957  caussi 7958  causs 7959  lmfex 7963  cmsmet 7965  metelcls 7969  metcld 7971  metcn4 7975  metcn4i 7976  oprcn 7981  opr1cn 7982  opr2cn 7983  opr1scn 7984  addcn 7990  subcn 7991  mulcn 7992  fsumcnlem 7993  fsumcn 7994  iscms2 7998  lmcau 8000  cmsss 8001  bcthlem32 8034  bcth 8036  grprndm 8058  0ngrp 8059  grprn 8060  grprcan 8066  grpinvval 8070  grpinvcl 8071  grpinvid 8077  grplcan 8078  grpasscan1 8080  grp2inv 8081  grpinvf 8082  grpinvop 8083  grpdivfval 8084  grpdivval 8085  grpdivf 8088  grpdivdiv 8090  grpmuldivass 8091  grpdivid 8092  grppncan 8093  grpnpcan 8094  grppnpcan2 8095  grpnnncan2 8096  resgrprn 8098  grplactval 8100  grplactf1o 8101  ablgrp 8105  abldivdiv4 8112  ablnncan 8115  subgres 8120  subgid 8123  subgabl 8126  cnid 8130  addinv 8131  readdsubg 8132  zaddsubg 8133  mulid 8135  ghgrpi 8140  ringabl 8153  vcabl 8179  vcm 8193  vcrinv 8194  vclinv 8195  vcoprnelem 8200  vcoprne 8201  vcex 8202  cnvc 8205  nvvop 8231  nvex 8233  nvvc 8237  nvabl 8238  nvsf 8241  nvscl 8250  nvsid 8251  nvsass 8252  nvdi 8254  nvdir 8255  nv2 8256  vsfval 8257  nvzcl 8258  nv0 8261  nvsz 8262  nvinv 8263  invfval 8264  nvmval 8266  nvmfval 8267  nvzs 8268  nvmf 8269  nvnnncan1 8271  nvnnncan2 8272  nvmdi 8273  nvnegneg 8274  nvrinv 8276  nvlinv 8277  nvsubadd 8278  nvpncan2 8279  nvaddsub4 8284  nvsubsub23 8285  nvnncan 8286  nvmeq0 8287  nvmid 8288  nvf 8289  nvdm 8292  nvs 8293  nvsub 8298  nvz0 8299  nvz 8300  nvtri 8301  nvmtri 8302  nvmtri2 8303  nvabs 8304  nvge0 8305  nvop 8308  nvoprne 8309  cnnvg 8311  cnnvba 8312  cnnvdemo 8313  cnnvs 8314  cnnvnm 8315  cnnvm 8316  elimnvu 8318  imsdval2 8321  nvnd 8322  imsdf 8323  imsmet 8327  nvelbl 8328  nvelbl2 8329  nvcnf 8330  nvcnpf 8331  nvcni 8332  nvcni2 8333  nvcni3 8334  nvlmcl 8335  nvlmle 8336  cnims 8337  sqcn 8338  sqcn2 8339  nmcni 8341  nmcn 8342  nmcn2 8343  nmcn3 8344  nmcnc 8345  abscn 8346  abscncfALT 8347  va1cnlem 8348  va1cn 8349  sm1cnilem 8350  sm1cni 8351  ipfval 8355  ipval 8356  ipid 8366  ipcl 8368  ipf 8369  ipcj 8370  ip0r 8373  ipz 8375  ip1cnilem2 8377  ip1cnilem3 8378  ip1cnilem4 8379  ip1cnilem5 8380  ip1cni 8382  sspval 8385  sspid 8387  sspnv 8388  sspba 8389  sspg 8390  ssps 8392  sspmlem 8394  sspmval 8395  sspm 8396  sspz 8397  sspn 8398  sspival 8400  sspi 8401  sspimsval 8402  sspims 8403  lnoval 8416  lnof 8419  lno0 8420  lnocoi 8421  lnoadd 8422  lnosub 8423  lnomul 8424  nvcnpi3 8425  nvcnpi4 8426  nvo00 8427  nmoval 8429  nmosetn0 8431  nmoxr 8432  nmoge0 8433  nmorepnf 8434  nmolb 8437  isblo2 8446  bloln 8447  blof 8448  nmblore 8449  0oo 8452  0lno 8453  nmo0 8454  0blo 8455  nmlno0lem 8456  nmlno0i 8457  nmlno0 8458  nmlnoubi 8459  nmlnogt0 8460  lnon0 8461  nmblolbii 8462  nmblolbi 8463  isblo3i 8464  blometi 8466  blocnilem 8467  blocni 8468  blocn 8470  blocn2 8471  phop 8480  cnph 8481  elimphu 8483  isph 8484  ip0i 8487  ip1i 8489  ip2i 8490  ipdirilem 8491  ipdiri 8492  ipasslem1 8493  ipasslem2 8494  ipasslem6 8498  ipasslem7 8499  ipasslem8 8500  ipasslem9 8501  ipasslem11 8503  ipassi 8504  ipdir 8505  ipass 8508  ipsubdir 8511  siii 8516  sii 8517  sspph 8518  ipblnfi 8519  ip2eqi 8520  phoeqi 8521  ajfuni 8523  ajfun 8524  bnnv 8529  cnbn 8531  ubthlem3 8534  ubthlem4 8535  ubthlem6 8537  ubthlem9 8540  ubthlem11 8542  ubthlem12 8543  ubthlem13 8544  ubthlem14 8545  ubthii 8546  ubthi 8547  minveclem1 8548  minveclem2 8549  minveclem3 8550  minveclem9 8556  minveclem16 8563  minveclem21 8568  minveclem23 8570  minveclem28 8575  minveclem29 8576  minveclem33 8580  minvecex 8581  minveclem37 8584  minveceu 8586  minvecex2 8591  hlipgt0 8619  hlcompl 8620  htthlem4 8626  htthlem5 8627  htthlem12 8634  htthi 8635  pstr 8655  spwval2 8656  spwval 8662  spwnex 8664  spwpr4OLD 8665  spwpr4aOLD 8666  sincnlem 8668  sinco 8669  cosco 8670  sincn 8671  coscn 8672  pilem2 8674  pilem3 8675  pilem4 8676  sineq0 8715  efghgrpilem 8721  efghgrpi 8722  efifolem1 8724  efifolem4 8727  shftefif1olem 8743  shftefif1o 8744  eff1oi 8748  eff1o 8750  h2hva 8845  h2hsm 8846  h2hnm 8847  h2hvs 8848  axhcompl 8870  hiidrclt 8963  normlem7 8984  norm-ii 9006  hilid 9030  hilvc 9031  hilnorm 9032  hhba 9036  hh0v 9037  hhims 9041  hhims2 9042  hhip 9046  hhph 9047  bcsHIL 9049  hilmet 9063  hilmetdval 9064  hilmetba 9065  hhhl 9075  hilcms 9076  hilhl 9077  hhssva 9131  hhsssm 9132  hhssnm 9133  hhssabl 9134  hhssnv 9136  hhssnvt 9137  hhsst 9138  hhshsslem1 9139  hhshsslem2 9140  hhsssh 9141  hhsssh2 9142  hhssba 9143  hhssvs 9144  hhssph 9146  hhssims 9147  hhssims2 9148  hhssbn 9153  occllem7 9181  projlem8 9195  projlem10 9197  projlem31 9218  projlem 9219  projlemHIL 9220  pjthlem13 9233  pjth 9235  pjvalt 9241  shsvat 9286  hosvalt 9518  hosvaltOLD 9519  homvalt 9520  hodvalt 9521  hodvaltOLD 9522  hfsvalt 9523  hfmvalt 9524  pjcomp 9621  dfiop2 9681  hoaddclt 9686  homulclt 9687  hoeqt 9688  hodseq 9722  ho01 9756  hoeq1t 9758  nmopsetretHIL 9793  nmopsetn0 9794  nmfnsetn0 9807  hhlno 9828  hhblo 9830  hh0o 9831  nmoplbt 9833  nmopub2tHIL 9836  nmfnlbt 9850  bravalvalt 9870  brafnt 9873  kbopt 9879  kbvalvalt 9880  kbpjt 9882  eigvalt 9886  hmopbdopHIL 9914  nmlnop0ALT 9922  nmlnop0HIL 9923  lnopco0 9931  nmcopex 9959  lnopcon 9965  nmcfnex 9988  lnfncon 9992  cnlnadj 10011  nmopadjle 10023  kbass2t 10052  kbass5t 10055  leopsqt 10064  hmopidmpj 10082  hmopidmcht 10083  hmopidmpjt 10084  pjssdif2 10104  pjinvar 10122  str 10187  hstr 10195  goeq 10203  irred 10324  mdsymlem8 10340  mdsym 10341  cdj3lem2 10365  elghom 10387  ghomgrpilem2 10389  ghomgrpi 10390  ghomgrplem 10392  ghomgrp 10393  ghomfo 10394  ghomlin 10396  ghomid 10397  ghomgsg 10398  ghomf1o 10400  symgoprval 10407  symggrpi 10409  symgidi 10410  cayleylem2 10413  cayleylem3 10414  cayleyi 10415  cayleyth 10417  cnrsfin 10503  cnrscoa 10504  mapdiscn 10505  hmeocna 10513  hmeocnb 10514  cmphmp 10515  cnvhmpha 10519  cnvhmphb 10520  cnvhmph 10521  hmphsyma 10522  hmphre 10524  hmeogrp 10532  homcard 10533  top2ind 10542  subsp 10548  filesn 10553  filint 10556  fipfil2 10558  emnfil 10559  oefil2 10560  neifil 10561  filintf 10562  fgsb 10563  filint2 10565  fgsb2 10568  rcfpfil 10577  limfillem2OLD 10587  dtopcl 10594  t2t1 10595  dtt2 10597  cnvtr 10617  doma 10640  coda 10641  ida 10642  cmppfa 10644  dcsda 10645  1ded 10650  dedalg 10655  idosd 10656  cmppfd 10657  domcmpd 10658  codcmpd 10659  rdmob 10660  rcmob 10661  aidm 10662  0ded 10669  0cat 10670  catded 10676  cmpasso 10685  cmpidb 10687  dmo 10688  cdmo 10689  jdmo 10690  cmpmorp 10691  ishomd 10697  ehm 10698  dehm 10699  cehm 10700  mrdmcd 10701  eqidob 10702  homib 10703  hine 10704  cmphmia 10705  cmphmib 10706  iri 10707  cmpassoh 10708  homgrf 10709  imonclem 10720  ismonc 10721  idmon 10724  immon 10725  fmamo 10735  vidfunid 10736  iddvvidd 10737  idcvvidc 10738  idfisf 10739  hgrablkne0 10752  emhgrat 10754

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

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

Copyright terms: Public domain