Theorem cleqid 1102

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

Assertion

Ref	Expression
cleqid	|- A = A

Proof of Theorem cleqid

Step	Hyp	Ref	Expression
1		pm4.2 148	. 2 |- (x e. A <-> x e. A)
2	1	cleqri 1101	1 |- A = A

Syntax hints:   = wceq 1091   e. wcel 1092

This theorem is referenced by:  visset 1350  ssid 1519  dfnul2 1709  dfnul3 1710  noel 1711  npss0 1731  snidg 1828  pri1 1841  snsspr 1853  int0 1978  syl5eqbr 2089  syl5eqbrr 2090  syl6breq 2093  biopabi 2103  so 2152  nlim0 2282  ordun 2332  dm0 2542  dmsn0 2543  dmsnsn0 2544  dmi 2545  funfn 2689  funex 2741  f0 2772  fnforn 2791  funforn 2792  f1orn 2809  f1o00 2823  f1o0 2824  funfvop 2857  fnopabfv 2858  funfv 2862  fvco 2865  fvopab4g 2870  fvreseq 2882  fvi 2900  fconst2 2902  tfr1 2962  tfr2 2963  tfr3 2964  tz7.44-1 2966  rdglem1 2975  bioprabi 3027  oprabval2g 3050  oprabval3 3052  f1stres 3096  1st2val 3097  df1st2 3098  0lt1o 3116  oe0m 3127  oawordeu 3157  ecelqsi 3229  ecoptocl 3239  ecopoprsym 3246  ecopoprtrn 3247  th3qlem2 3251  th3q 3253  en2d 3303  en2 3305  en3 3306  dom2d 3307  dom2 3308  pw2en 3348  sbth 3359  mapenlem2 3385  mapen 3386  mapxpen 3390  xpmapenlem4 3394  xpmapen 3396  unbnn 3435  unfilem3 3440  inf0 3457  inf3 3471  inf5 3472  tz9.1 3490  tz9.12 3506  ssrankr1 3520  rankel 3524  rankpw 3528  r1rankid 3537  scott0 3542  cplem2 3546  aceq3 3556  aceq4 3557  aceq5 3563  aceq6a 3564  aceq6b 3565  ac6 3576  aceqkm 3596  numth 3599  weth 3602  zornlem6 3608  zorn2lem 3610  zorn 3611  unxpdomlem 3649  0npi 3804  recidpq 3865  0npr 3890  genpprecl 3898  00sr 4002  opelreal 4043  eqresr 4049  subaddeq 4146  divcan2 4224  leidt 4293  nnleltp1t 4448  creur 4532  creui 4533  0nn0 4546  0z 4573  uzwo3 4616  zmin 4617  znq 4630  seq1 4670  seqsuc 4671  seqfn 4672  discrlem2 4714  discrlem 4716  sqrlem21 4751  sqrsqid 4766  replimt 4798  clim0 4882  ruclem14 4898  ruclem15 4899  ruclem38 4922  nnenom 4926  qnnen 4931  infxpidmlem9 4941  infxpidm 4945  infmap2 4953  normlem7 5069  norm-ii 5086  bcs 5101  occllem7 5186  projlem8 5200  projlem10 5202  projlem31 5223  projlem 5224  pjthlem13 5237  pjth 5239  pjvalt 5246  shsvat 5285  chocnul 5293  hosmvalt 5487  hodmvalt 5488  hosvalt 5489  hodvalt 5490  pjcomp 5565  hoeq 5595  ho1 5613  hodseq 5619  pjnel 5665  str 5698  goeq 5706  mdsymlem8 5783  mdsym 5784

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-gen 677  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-cleq 1097

metamath.org