Theorem eqid 2040

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). (Thanks to Stefan Allan and BJ for this information.) (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 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 160	. 2 |- ( x e. A <-> x e. A )
2	1	eqriv 2037	1 |- A = A

Syntax hints:   = wceq 1243   e. wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  eqidd  2041  neirr  2215  sbsbc  2768  sbceqal  2814  dfnul2  3226  snidg  3400  prid1g  3474  tpid1  3481  tpid2  3482  tpid3  3484  dfiin2g  3690  syl5eqbr  3797  syl5eqbrr  3798  syl6breq  3803  opabbii  3824  mpteq2ia  3843  mpteq2da  3846  sucidg  4153  onsucelsucexmidlem1  4253  regexmidlemm  4257  regexmidlem1  4258  reg2exmidlema  4259  regexmid  4260  reg2exmid  4261  reg3exmid  4304  tfisi  4310  finds1  4325  nn0suc  4327  nndceq0  4339  0elnn  4340  nnregexmid  4342  opelxp  4374  relopab  4464  relop  4486  ididg  4489  elrnmpt1s  4584  dfiun3g  4589  dfiin3g  4590  dmmptg  4818  funfn  4931  mpt0  5026  f0  5080  dffn4  5112  f1orn  5136  f1oabexg  5138  f1o00  5161  f1o0  5163  fnbrfvb  5214  fnrnfv  5220  funfvdm  5236  fvmptg  5248  fvmptd  5253  fvmpt2d  5257  fvmptdf  5258  mpteqb  5261  fvmptt  5262  funfvop  5279  eldmrexrn  5308  fmpt2d  5327  fmptco  5330  fmptcof  5331  fnasrn  5341  fnasrng  5343  mptexg  5386  eufnfv  5389  idref  5396  f1elima  5412  fliftrel  5432  fliftel  5433  fliftel1  5434  fliftcnv  5435  fliftf  5439  riotabiia  5485  acexmidlem2  5509  acexmidlemv  5510  oprabbii  5560  mpt2eq12  5565  ovmpt2dxf  5626  ovmpt2df  5632  ov6g  5638  f1ocnvd  5702  f1opw2  5706  suppssfv  5708  suppssov1  5709  fnofval  5721  off  5724  offval2  5726  ofrfval2  5727  caofinvl  5733  abrexex  5744  abrexexg  5745  offres  5762  ofmres  5763  op1steq  5805  reldm  5812  mpt2exga  5835  mpt2ex  5836  fmpt2co  5837  cnvf1o  5846  tposssxp  5864  brtpos2  5866  tpos0  5889  iunon  5899  tfr2a  5936  tfrlemisucfn  5938  tfri1d  5949  tfrex  5954  tfrfun  5955  rdgfun  5960  rdg0  5974  frec0g  5983  frecfnom  5986  frecsuclem1  5987  frecsuclemdm  5988  frecsuclem3  5990  0lt1o  6023  oafnex  6024  omfnex  6029  fnoei  6032  oeiexg  6033  oeiv  6036  oacl  6040  omcl  6041  oeicl  6042  oav2  6043  omv2  6045  eqer  6138  ecelqsg  6159  elqsn0m  6174  qsel  6183  qliftf  6191  ecoptocl  6193  eroprf  6199  ecopovsym  6202  ecopovtrn  6203  ecopovsymg  6205  ecopovtrng  6206  th3qlem2  6209  th3q  6211  en2d  6248  en3d  6249  dom2lem  6252  dom2  6255  xpcomen  6301  fidifsnen  6331  0npi  6411  indpi  6440  recidnq  6491  addnnnq0  6547  mulnnnq0  6548  genpprecll  6612  genppreclu  6613  caucvgprpr  6810  addsrpr  6830  mulsrpr  6831  0nsr  6834  00sr  6854  caucvgsrlemgt1  6879  opelreal  6904  eqresr  6912  axprecex  6954  nntopi  6968  ltxrlt  7085  pncan3  7219  apreim  7594  divcanap2  7659  divcanap3  7675  nn1gt1  7947  0nn0  8196  0z  8256  4t4e16  8440  5t4e20  8442  6t3e18  8445  6t4e24  8446  6t5e30  8447  7t3e21  8450  7t4e28  8451  7t5e35  8452  7t6e42  8453  7t7e49  8454  8t3e24  8456  8t4e32  8457  8t5e40  8458  8t7e56  8460  8t8e64  8461  9t3e27  8463  9t4e36  8464  9t5e45  8465  9t6e54  8466  9t7e63  8467  9t8e72  8468  9t9e81  8469  znq  8559  ltpnf  8702  mnflt  8704  mnfltpnf  8706  xnegpnf  8741  xnegmnf  8742  lincmb01cmp  8871  iccf1o  8872  elfzuz2  8893  fseq1m1p1  8957  fz0tp  8981  flqdiv  9163  frecuzrdgrrn  9194  uzenom  9202  fzfig  9206  nnenom  9210  iseqeq1  9214  iseqeq4  9217  iseqval  9220  iseqfn  9221  iseq1  9222  iseqcl  9223  iseqp1  9225  monoord2  9236  iseqdistr  9249  serile  9253  exp0  9259  0exp  9290  sq0  9344  shftfibg  9421  shftfib  9424  shftfn  9425  2shfti  9432  cvg1n  9585  resqrexlemsqa  9622  climconst2  9812  climres  9824  climshft  9825  iserclim0  9826  climle  9854  clim2iser  9857  clim2iser2  9858  climub  9864  climcvg1n  9869  climcaucn  9870  serif0  9871  ex-or  9893  ex-an  9894  bj-2inf  10062  bj-inf2vnlem1  10095