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

Syntax hints:   = wceq 1642   e. 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  2522  vex  2863  reu6  3026  sbsbc  3051  sbceqal  3098  dfnul2  3553  dfnul3  3554  snidg  3759  prid1g  3826  tpid1  3830  tpid2  3831  tpid3  3833  int0  3941  dfiin2g  4001  opkth1g  4131  snel1c  4141  opkabssvvk  4209  eladdci  4400  nnc0suc  4413  elsuci  4415  nulel0c  4423  0fin  4424  nnsucelr  4429  lefinaddc  4451  tfinnul  4492  opabbii  4627  syl5eqbr  4673  syl5eqbrr  4674  syl6breq  4679  ididg  4872  xpcan  5058  xpcan2  5059  funfn  5137  dffn4  5276  f1orn  5297  f1o00  5318  tz6.12i  5349  dffn5  5364  funfv  5376  fvopab4g  5389  funfvop  5401  funiunfv  5468  f1elima  5475  1stfo  5506  2ndfo  5507  swapf1o  5512  opfv1st  5515  opfv2nd  5516  oprabbii  5566  ov2ag  5599  ov6g  5601  mpteq2ia  5660  mpt2eq12  5663  mpteq2da  5667  dmmptg  5685  fvmptd  5703  fvmptnf  5724  f1od  5727  op1st2nd  5791  clos1basesucg  5885  dfnnc3  5886  ecelqsg  5980  elqsn0  5994  qsdisj  5996  ecoptocl  5997  enmap2  6069  enmap1  6075  enprmaplem6  6082  enprmap  6083  nenpw1pw  6087  enpw  6088  nulnnc  6119  ncspw1eu  6160  pw1eltc  6163  ce2  6193  ce2ncpw11c  6195  sbthlem2  6205  sbthlem3  6206  tce2  6237  spacssnc  6285  spacid  6286  spaccl  6287  spacind  6288  nchoicelem3  6292  frecxp  6315  frecxpg  6316  dmfrec  6317  fnfreclem2  6319  fnfreclem3  6320  frecsuc  6323  dmsnfn  6328  scancan  6332