Theorem eqidd 2116

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

Assertion

Ref	Expression
eqidd	|- ( ph -> A = A )

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2115	. 2 |- A = A
2	1	a1i 9	1 |- ( ph -> A = A )

Syntax hints:   -> wi 4   = wceq 1314

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

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

This theorem is referenced by:  cbvraldva  2634  cbvrexdva  2635  rspcedeq1vd  2768  rspcedeq2vd  2769  nelrdva  2860  opeq2  3672  mpteq1  3972  tfisi  4461  feq23d  5226  fvmptdv2  5464  elrnrexdm  5513  fmptco  5540  cofmpt  5543  ftpg  5558  fliftfun  5651  fliftval  5655  cbvmpo  5804  fconstmpo  5820  eqfnov2  5832  ovmpod  5852  ovmpodv2  5858  ofvalg  5945  ofrval  5946  off  5948  ofres  5950  suppssof1  5953  ofco  5954  caofref  5957  caofrss  5960  caoftrn  5961  rdgivallem  6232  iserd  6409  ixpsnf1o  6584  1domsn  6666  mapxpen  6695  ctssexmid  6974  infrenegsupex  9291  fzo0to3tp  9889  modqsubmod  10048  0tonninf  10105  iseqovex  10122  seqvalcd  10125  seq3f1olemqsumkj  10164  seq3id  10174  seq3id2  10175  resqrexlemp1rp  10670  resqrexlemfp1  10673  resqrex  10690  infxrnegsupex  10924  climcl  10943  clim2  10944  climuni  10954  climeq  10960  2clim  10962  climshftlemg  10963  climabs0  10968  climcn1  10969  climcn2  10970  climge0  10986  climsqz  10996  climsqz2  10997  climcau  11008  climrecvg1n  11009  climcaucn  11012  serf0  11013  isumz  11050  fisumss  11053  fsumsplitsn  11071  fsumsplitsnun  11080  isumclim3  11084  isummulc2  11087  fsum2dlemstep  11095  fsumconst  11115  fsumabs  11126  fsumparts  11131  iserabs  11136  fsumiun  11138  isumshft  11151  cvgratnnlemseq  11187  mertenslemub  11195  mertenslemi1  11196  mertenslem2  11197  eftlcl  11245  reeftlcl  11246  eftlub  11247  efsep  11248  effsumlt  11249  eirraplem  11331  2tp1odd  11429  bezoutlemstep  11531  alginv  11574  algfx  11579  cncongr1  11630  qnumdencoprm  11716  qeqnumdivden  11717  unct  11797  epttop  12102  lmss  12257  txlm  12290  lmcn2  12291  cnmpt2c  12301  blfvalps  12374  bdxmet  12490  fsumcncntop  12542  cncfmptc  12568  cncfmpt1f  12570  cdivcncfap  12573  negfcncf  12575  dvidlemap  12615  dvcnp2cntop  12618  dvaddxxbr  12620  dvmulxxbr  12621  dviaddf  12624  nninfsellemeqinf  12904  nninffeq  12908  exmidsbthrlem  12909  cvgcmp2nlemabs  12919