Theorem eqidd 2171

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	⊢ (𝜑 → 𝐴 = 𝐴)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2170	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 9	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  cbvraldva  2705  cbvrexdva  2706  rspcedeq1vd  2843  rspcedeq2vd  2844  nelrdva  2937  opeq2  3766  mpteq1  4073  tfisi  4571  feq23d  5343  fvmptdv2  5585  elrnrexdm  5635  fmptco  5662  cofmpt  5665  ftpg  5680  fliftfun  5775  fliftval  5779  cbvmpo  5932  fconstmpo  5948  eqfnov2  5960  ovmpod  5980  ovmpodv2  5986  ofvalg  6070  ofrval  6071  off  6073  ofres  6075  suppssof1  6078  ofco  6079  caofref  6082  caofrss  6085  caoftrn  6086  rdgivallem  6360  iserd  6539  ixpsnf1o  6714  1domsn  6797  mapxpen  6826  infnninf  7100  ctssexmid  7126  nninfdcinf  7147  nninfwlporlemd  7148  nninfwlporlem  7149  nninfwlpoimlemginf  7152  infrenegsupex  9553  fz0to4untppr  10080  fzo0to3tp  10175  modqsubmod  10338  0tonninf  10395  iseqovex  10412  seqvalcd  10415  seq3f1olemqsumkj  10454  seq3id  10464  seq3id2  10465  resqrexlemp1rp  10970  resqrexlemfp1  10973  resqrex  10990  infxrnegsupex  11226  climcl  11245  clim2  11246  climuni  11256  climeq  11262  2clim  11264  climshftlemg  11265  climabs0  11270  climcn1  11271  climcn2  11272  climge0  11288  climsqz  11298  climsqz2  11299  climcau  11310  climrecvg1n  11311  climcaucn  11314  serf0  11315  isumz  11352  fisumss  11355  fsumsplitsn  11373  fsumsplitsnun  11382  isumclim3  11386  isummulc2  11389  fsum2dlemstep  11397  fsumconst  11417  fsumabs  11428  fsumparts  11433  iserabs  11438  fsumiun  11440  isumshft  11453  cvgratnnlemseq  11489  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  prod1dc  11549  fprodssdc  11553  fprodunsn  11567  fprodcl2lem  11568  fprodconst  11583  fprod2dlemstep  11585  fprodsplitsn  11596  eftlcl  11651  reeftlcl  11652  eftlub  11653  efsep  11654  effsumlt  11655  eirraplem  11739  2tp1odd  11843  bezoutlemstep  11952  alginv  12001  algfx  12006  cncongr1  12057  qnumdencoprm  12147  qeqnumdivden  12148  ctiunctal  12396  unct  12397  nninfdclemcl  12403  nninfdclemf  12404  nninfdclemp1  12405  nninfdc  12408  issgrp  12644  sgrp1  12651  ismndd  12673  mndprop  12677  insubm  12703  grpprop  12725  grpsubfvalg  12748  epttop  12884  lmss  13040  txlm  13073  lmcn2  13074  cnmpt2c  13084  txswaphmeolem  13114  blfvalps  13179  bdxmet  13295  fsumcncntop  13350  cncfmptc  13376  cncfmpt1f  13378  cdivcncfap  13381  negfcncf  13383  dvidlemap  13454  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dviaddf  13463  dvexp  13469  dvmptaddx  13475  dvmptmulx  13476  dvef  13482  sincn  13484  coscn  13485  lgsdir2lem5  13727  2sqlem8  13753  nninfsellemeqinf  14049  nninffeq  14053  exmidsbthrlem  14054  cvgcmp2nlemabs  14064