Theorem eqid 2353

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

This law is thought to have originated with Aristotle (Metaphysics, Zeta, 17, 1041 a, 10-20: "Therefore, inquiring why a thing is itself, it's inquiring nothing; ... saying that the thing is itself constitutes the sole reasoning and the sole cause, in every case, to the question of why the man is man or the musician musician."). (Thanks to Stefan Allan and Benoît Jubin for this information.) (Contributed by NM, 5-Aug-1993.) (Revised by Benoît Jubin, 14-Oct-2017.)

Assertion

Ref	Expression
eqid	⊢ A = A

Proof of Theorem eqid

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		biid 227	. 2 ⊢ (x ∈ A ↔ x ∈ A)
2	1	eqriv 2350	1 ⊢ A = A

Syntax hints:   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-cleq 2346

This theorem is referenced by:  eqidd  2354  neirr  2521  vex  2862  reu6  3025  sbsbc  3050  sbceqal  3097  dfnul2  3552  dfnul3  3553  snidg  3758  prid1g  3825  tpid1  3829  tpid2  3830  tpid3  3832  int0  3940  dfiin2g  4000  opkth1g  4130  snel1c  4140  opkabssvvk  4208  eladdci  4399  nnc0suc  4412  elsuci  4414  nulel0c  4422  0fin  4423  nnsucelr  4428  lefinaddc  4450  tfinnul  4491  opabbii  4626  syl5eqbr  4672  syl5eqbrr  4673  syl6breq  4678  ididg  4871  xpcan  5057  xpcan2  5058  funfn  5136  dffn4  5275  f1orn  5296  f1o00  5317  tz6.12i  5348  dffn5  5363  funfv  5375  fvopab4g  5388  funfvop  5400  funiunfv  5467  f1elima  5474  1stfo  5505  2ndfo  5506  swapf1o  5511  opfv1st  5514  opfv2nd  5515  oprabbii  5565  ov2ag  5598  ov6g  5600  mpteq2ia  5659  mpt2eq12  5662  mpteq2da  5666  dmmptg  5684  fvmptd  5702  fvmptnf  5723  f1od  5726  op1st2nd  5790  clos1basesucg  5884  dfnnc3  5885  ecelqsg  5979  elqsn0  5993  qsdisj  5995  ecoptocl  5996  enmap2  6068  enmap1  6074  enprmaplem6  6081  enprmap  6082  nenpw1pw  6086  enpw  6087  nulnnc  6118  ncspw1eu  6159  pw1eltc  6162  ce2  6192  ce2ncpw11c  6194  sbthlem2  6204  sbthlem3  6205  tce2  6236  spacssnc  6284  spacid  6285  spaccl  6286  spacind  6287  nchoicelem3  6291  frecxp  6314  frecxpg  6315  dmfrec  6316  fnfreclem2  6318  fnfreclem3  6319  frecsuc  6322  dmsnfn  6327  scancan  6331