Theorem eqid 1452

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

Syntax hints:   = wceq 1099   e. wcel 1105

This theorem is referenced by:  visset 1788  reu3 1902  sbcbii 1949  ssid 2051  uniiunlem 2103  dfnul2 2253  dfnul3 2254  noel 2255  npss0 2280  ifor 2352  snidg 2404  pri1 2420  snsspr 2440  int0 2515  syl5eqbr 2616  syl5eqbrr 2617  syl6breq 2622  ssbri 2625  opabbii 2639  so 2828  unisn2 2839  ralxfrALT 2863  nlim0 2990  ordun 3044  finds1 3122  issetid 3237  dm0 3280  dmsn0 3281  dmsnsn0 3282  dmi 3283  funfn 3483  f0 3595  fnforn 3616  f1orn 3637  f1oabexg 3639  f1o00 3653  f1o0 3655  funbrfvb 3694  fnopabfv 3697  funfv 3709  fvco 3713  fvopab4g 3718  fvopab4gf 3720  fvreseq 3738  fvimacnvALT 3748  fopabco 3771  fopabcos 3772  fopabsn 3779  fvi 3781  fconst2g 3784  funiunfv 3805  tfr1 3863  tfr2 3864  tfr3 3865  tz7.44-1 3867  rdglem1 3876  oprabbii 3936  oprabval2gf 3965  oprabval3 3969  oprabval6g 3971  1st2val 4033  2nd2val 4034  curry1 4036  curry1f 4037  curry1val 4038  df1st2 4064  df2nd2 4065  0lt1o 4085  oe0m 4095  oawordeu 4127  nneob 4193  ecelqsi 4230  ecoptocl 4241  ecopoprsym 4248  ecopoprtrn 4249  th3qlem2 4253  th3q 4255  en2d 4335  en2 4337  en3 4338  dom2d 4339  dom2 4340  pw2en 4380  sbth 4391  mapenlem2 4422  mapen 4423  mapxpen 4427  xpmapenlem4 4431  xpmapen 4433  unbnn 4473  unfilem3 4478  abfii3 4489  iunfi 4495  pwfi 4497  inf0 4530  inf3 4544  infeq5 4545  tz9.1 4570  tz9.12 4586  ssrankr1 4600  rankel 4604  rankpw 4608  r1rankid 4618  scott0 4641  cplem2 4645  aceq3 4657  aceq4 4658  aceq5 4664  aceq6a 4665  aceq6b 4666  ac6 4679  aceqkm 4705  numth 4708  weth 4711  zorn2lem6 4717  zornlem 4719  zorn2 4720  brdom7disj 4728  brdom6disj 4729  iundom 4736  unxpdomlem 4766  alephfp2 4824  dominf 4827  0npi 4933  recidpq 4994  0npr 5019  genpprecl 5027  00sr 5131  opelreal 5172  eqresr 5178  ltsor 5184  pncan3t 5300  leidt 5455  renfdisj 5463  ltpnft 5466  mnfltt 5467  mnfltpnf 5468  xrleidt 5484  divcan2 5636  nnleltp1t 5852  0nn0 6011  0z 6044  uzwo3 6117  zmin 6118  znq 6147  seq11 6205  seq1p1 6206  seq1fn 6208  seq1res 6215  shftfn 6231  shftvalt 6234  seq1shftid 6244  icoshftf1o 6295  seq1seqz 6424  seq1seq0 6428  seqzeq 6438  seqzres 6443  seqzres2 6444  dfseq0 6446  exp0t 6454  0expt 6472  sq0 6517  discrlem2 6538  discrlem 6540  sqrlem21 6574  sqrmsq 6590  replimt 6643  abs0 6765  fsum1 6894  fsump1 6895  fsumconst 6927  climsub 7017  climcmp 7025  caucvg2 7052  caucvg3 7054  iserzabs 7066  cvgcmp2 7068  cvgcmp2c 7070  cvgcmp3ce 7074  isumclim5t 7088  isumshft 7090  isumshft2 7091  isummulc1 7098  isummulc1ALT 7099  infcvgaux1 7105  infcvgaux2 7106  infcvg 7110  geolimi 7122  geolim 7123  geolim1i 7124  geolim1 7125  geosum 7127  geoisum 7128  geoisum1 7130  geoisum1c 7131  cvgratlem5 7140  cvgrat 7141  divccncf 7166  ivthlem8 7174  isupivth 7176  dsupivth 7178  ivthlem8OLD 7183  ivthOLD 7184  efseq1ex 7199  dfef2 7200  efclt 7205  efcvgfsum 7208  reefcl 7210  erelem2 7213  erelem6 7217  ereALT 7224  ege2 7225  ele3 7226  ege2le3 7227  ef0 7228  efcj 7229  efaddlem23 7253  efaddlem27 7257  efaddlem28 7258  efadd 7259  eftlext 7271  ef1tlub 7275  ef01tllem2 7277  ef01tlub 7278  absef01tlub 7280  eirrlem3 7283  eirr 7286  ef4p 7291  ef4pt 7292  efge1 7293  efge1p 7294  absefm1le 7303  eflegeo 7306  efcnlem3 7312  reeff1olem2 7316  reeff1olem2OLD 7318  sin01bndlem2 7361  cos01bndlem2 7363  sin01bnd 7365  cos01bnd 7366  acdc3lem 7379  acdc3 7380  acdc2lem2 7382  acdc2 7383  acdc5lem2 7385  acdc5 7386  acdclem 7387  acdc 7388  acdcALT 7389  nnenom 7391  qnnen 7397  unben 7399  infpn 7402  ruclem15 7418  ruclem38 7441  infxpidmlem9 7454  infxpidm 7458  infmap2 7474  eltopsp 7497  tpsex 7498  istps2 7500  basgen2t 7532  ntrval 7569  clsval 7570  0cld 7571  iincld 7572  uncld 7574  cldcls 7575  neival 7606  neii2 7611  neiss 7612  opnneiss 7621  innei 7625  neissex 7627  lpval 7632  qdensere 7639  cnpval 7647  cnpimaex 7652  cnima 7654  cnco 7655  cnpco 7656  cnclima 7658  haustop 7673  dfms2 7686  met0 7702  metres 7711  metxpcl 7720  metxplem4 7721  metxp 7722  blfval 7723  blval 7725  blrn 7729  blf 7732  blelrn 7736  blss 7741  opni 7752  opni2 7753  opni3 7754  blssopn 7755  opnuni 7756  opnin 7757  unirnbl 7763  neibl 7765  lpbl 7767  methausi 7768  methaus 7769  metcnpf 7770  metcnf 7771  metcnconst 7772  metcnp 7774  metcn 7776  metcnss 7785  metcnss2 7786  metidcn 7787  metdnsconst 7788  cncfmet 7792  remetdval 7795  remet 7797  tgioo 7802  lmrel 7813  lmbr 7814  lmuni 7834  lmsslem 7835  lmss 7836  caussi 7837  causs 7838  lmfex 7842  cmsmet 7844  metelcls 7848  metcld 7849  metcn4 7853  metcn4i 7854  oprcn 7859  opr1cn 7860  opr2cn 7861  opr1scn 7862  addcn 7868  subcn 7869  mulcn 7870  fsumcnlem 7871  fsumcn 7872  iscms2 7876  lmcau 7878  cmsss 7879  bcthlem32 7912  bcth 7914  grprndm 7936  0ngrp 7937  grprn 7938  grprcan 7945  grpinvval 7949  grpinvcl 7950  grpinvid 7957  grplcan 7958  grpasscan1 7960  grp2inv 7961  grpinvf 7962  grpinvop 7963  grpdivfval 7964  grpdivval 7965  grpdivf 7968  grpdivdiv 7970  grpmuldivass 7971  grpdivid 7972  grppncan 7973  grpnpcan 7974  grppnpcan2 7975  grpnnncan2 7976  resgrprn 7978  resgrprnOLD 7979  grplactval 7981  grplactf1o 7982  ablgrp 7986  abldivdiv4 7994  ablnncan 7997  subgres 8002  subgid 8005  subgabl 8008  cnid 8012  addinv 8013  readdsubg 8014  zaddsubg 8015  mulid 8017  ghgrpi 8022  ringabl 8035  vcabl 8063  vcm 8077  vcrinv 8078  vclinv 8079  cnvc 8083  nvvop 8108  nvvc 8112  nvabl 8113  nvsf 8116  nvscl 8125  nvsid 8126  nvsass 8127  nvdi 8129  nvdir 8130  nv2 8131  vsfval 8132  nvzcl 8133  nv0 8136  nvsz 8137  nvinv 8138  nvmval 8140  nvmfval 8141  nvzs 8142  nvmf 8143  nvnnncan1 8145  nvnnncan2 8146  nvmdi 8147  nvnegneg 8148  nvrinv 8150  nvlinv 8151  nvsubadd 8152  nvpncan2 8153  nvaddsub4 8158  nvsubsub23 8159  nvnncan 8160  nvmeq0 8161  nvmid 8162  nvf 8163  nvs 8166  nvsub 8171  nvz0 8172  nvz 8173  nvtri 8174  nvmtri 8175  nvmtri2 8176  nvabs 8177  nvge0 8178  nvop 8181  cnnvg 8183  cnnvba 8184  cnnvdemo 8185  cnnvs 8186  cnnvnm 8187  cnnvm 8188  elimnvu 8190  imsdval2 8193  nvnd 8194  imsdf 8195  imsmet 8199  nvelbl 8200  nvelbl2 8201  nvcnf 8202  nvcni 8203  nvlmcl 8204  nvlmle 8205  cnims 8206  sqcn 8207  sqcn2 8208  nmcni 8210  nmcn 8211  nmcn2 8212  nmcnc 8213  va1cnlem 8214  va1cn 8215  sm1cnilem 8216  sm1cni 8217  ipfval 8221  ipval 8222  ipid 8232  ipcl 8234  ipf 8235  ipcj 8236  ip0r 8239  ipz 8241  ip1cnilem2 8243  ip1cnilem3 8244  ip1cnilem4 8245  ip1cnilem5 8246  ip1cni 8248  sspval 8251  sspid 8253  sspnv 8254  sspba 8255  sspg 8256  ssps 8258  sspmlem 8260  sspmval 8261  sspm 8262  sspz 8263  sspn 8264  sspival 8266  sspi 8267  sspimsval 8268  sspims 8269  lnoval 8282  lnof 8285  lno0 8286  lnocoi 8287  lnosub 8288  lnomul 8289  nvcnpi4 8290  nvo00 8291  nmoval 8293  nmosetn0 8295  nmoxr 8296  nmoge0 8297  nmorepnf 8298  nmolb 8301  isblo2 8310  bloln 8311  blof 8312  nmblore 8313  0oo 8316  0lno 8317  nmo0 8318  0blo 8319  nmlno0lem 8320  nmlno0i 8321  nmlno0 8322  nmlnoubi 8323  nmlnogt0 8324  nmblolbii 8325  nmblolbi 8326  isblo3i 8327  blometi 8329  blocnilem 8330  blocni 8331  blocn 8333  blocn2 8334  phop 8343  cnph 8344  elimphu 8346  isph 8347  ip0i 8350  ip1i 8352  ip2i 8353  ipdirilem 8354  ipdiri 8355  ipasslem1 8356  ipasslem2 8357  ipasslem6 8361  ipasslem7 8362  ipasslem8 8363  ipasslem9 8364  ipasslem11 8366  ipassi 8367  ipdir 8368  ipass 8371  ipsubdir 8374  siii 8379  sii 8380  sspph 8381  ipblnfi 8382  ip2eqi 8383  phoeqi 8384  ajfuni 8386  ajfun 8387  bnnv 8392  cnbn 8394  ubthlem3 8397  ubthlem4 8398  ubthlem6 8400  ubthlem9 8403  ubthlem11 8405  ubthlem12 8406  ubthlem13 8407  ubthlem14 8408  ubthii 8409  ubthi 8410  minveclem1 8411  minveclem2 8412  minveclem3 8413  minveclem9 8419  minveclem16 8426  minveclem21 8431  minveclem23 8433  minveclem28 8438  minveclem29 8439  minveclem33 8443  minvecex 8444  minveclem37 8447  minveceu 8449  minvecex2 8454  hlipgt0 8480  hlcompl 8481  htthlem4 8487  htthlem5 8488  htthlem12 8495  htthi 8496  sincnlem 8498  sinco 8499  cosco 8500  sincn 8501  coscn 8502  pilem2 8504  pilem3 8505  pilem4 8506  efghgrpilem 8547  efghgrpi 8548  efifolem1 8550  efifolem4 8553  shftefif1olem 8574  shftefif1olemOLD 8575  shftefif1o 8576  eff1oi 8581  eff1o 8583  elghom 8651  ghomgrpilem2 8653  ghomgrpi 8654  ghomgrplem 8656  ghomgrp 8657  ghomfo 8658  ghomlin 8660  ghomid 8661  ghomgsg 8662  ghomf1o 8664  symgoprval 8671  symgidi 8674  symggrp 8675  cayleylem2 8677  cayleylem3 8678  cayleyi 8679  cayleyth 8681  hmeocna 8757  hmeocnb 8758  cmphmp 8759  cnvhmpha 8763  cnvhmphb 8764  cnvhmph 8765  hmphsyma 8766  hmphre 8768  hmeogrp 8776  subsp 8779  filesn 8784  filint 8787  fipfil2 8789  emnfil 8790  oefil2 8791  neifil 8792  filintf 8793  fgsb 8794  filint2 8796  fgsb2 8799  dtopcl 8809  t2t1 8810  dtt2 8812  cnvtr 8832  doma 8855  coda 8856  ida 8857  cmppfa 8859  dcsda 8860  1ded 8865  dedalg 8870  idosd 8871  cmppfd 8872  domcmpd 8873  codcmpd 8874  rdmob 8875  rcmob 8876  aidm 8877  aidmold 8878  0ded 8884  0cat 8885  catded 8891  cmpasso 8900  cmpidb 8902  dmo 8903  cdmo 8904  jdmo 8905  cmpmorp 8906  ishomd 8912  ehm 8913  dehm 8914  cehm 8915  mrdmcd 8916  eqidob 8917  homib 8918  hine 8919  cmphmia 8920  cmphmib 8921  iri 8922  cmpassoh 8923  homgrf 8924  imonclem 8933  ismonc 8934  fmamo 8942  vidfunid 8943  hgrablkne0 8955  emhgrat 8957  hiidrclt 9110  normlem7 9131  norm-ii 9153  hilid 9177  hilvc 9178  hilnorm 9179  hhva 9182  hhba 9183  hh0v 9184  hhsm 9185  hhvs 9186  hhnm 9187  hhims 9188  hhims2 9189  hhip 9193  hhph 9194  bcsHIL 9196  hilmet 9212  hilmetdval 9213  hilmetba 9214  hhlm 9218  hhcau 9219  hhhl 9224  hilcms 9225  hilhl 9226  hhssva 9280  hhsssm 9281  hhssnm 9282  occllem7 9309  projlem8 9323  projlem10 9325  projlem31 9346  projlem 9347  pjthlem13 9360  pjth 9362  pjvalt 9368  shsvat 9413  hosvalt 9647  hosvaltOLD 9648  homvalt 9649  hodvalt 9650  hodvaltOLD 9651  hfsvalt 9652  hfmvalt 9653  pjcomp 9750  dfiop2 9810  hoaddclt 9815  homulclt 9816  hoeqt 9817  hodseq 9851  ho01 9885  hoeq1t 9887  nmopsetretHIL 9922  nmopsetn0 9923  nmfnsetn0 9936  hhlno 9957  hhblo 9959  hh0o 9960  nmoplbt 9962  nmfnlbt 9978  bravalvalt 9998  brafnt 10001  kbopt 10007  kbvalvalt 10008  kbpjt 10010  eigvalt 10014  hmopbdopHIL 10042  nmlnop0ALT 10049  nmlnop0HIL 10050  lnopco0 10058  nmcopex 10086  lnopcon 10092  nmcfnex 10115  lnfncon 10119  cnlnadj 10138  nmopadjle 10150  kbass2t 10176  kbass5t 10179  leopsqt 10188  hmopidmpj 10205  hmopidmcht 10206  hmopidmpjt 10207  pjssdif2 10227  pjinvar 10243  str 10308  hstr 10316  goeq 10324  irred 10443  mdsymlem8 10459  mdsym 10460  cdj3lem2 10481

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

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

Copyright terms: Public domain