Theorem eqidd 2138

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 2137	. 2 |- A = A
2	1	a1i 9	1 |- ( ph -> A = A )

Syntax hints:   -> wi 4   = wceq 1331

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 1425  ax-ext 2119

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

This theorem is referenced by:  cbvraldva  2658  cbvrexdva  2659  rspcedeq1vd  2793  rspcedeq2vd  2794  nelrdva  2886  opeq2  3701  mpteq1  4007  tfisi  4496  feq23d  5263  fvmptdv2  5503  elrnrexdm  5552  fmptco  5579  cofmpt  5582  ftpg  5597  fliftfun  5690  fliftval  5694  cbvmpo  5843  fconstmpo  5859  eqfnov2  5871  ovmpod  5891  ovmpodv2  5897  ofvalg  5984  ofrval  5985  off  5987  ofres  5989  suppssof1  5992  ofco  5993  caofref  5996  caofrss  5999  caoftrn  6000  rdgivallem  6271  iserd  6448  ixpsnf1o  6623  1domsn  6706  mapxpen  6735  ctssexmid  7017  infrenegsupex  9382  fzo0to3tp  9989  modqsubmod  10148  0tonninf  10205  iseqovex  10222  seqvalcd  10225  seq3f1olemqsumkj  10264  seq3id  10274  seq3id2  10275  resqrexlemp1rp  10771  resqrexlemfp1  10774  resqrex  10791  infxrnegsupex  11025  climcl  11044  clim2  11045  climuni  11055  climeq  11061  2clim  11063  climshftlemg  11064  climabs0  11069  climcn1  11070  climcn2  11071  climge0  11087  climsqz  11097  climsqz2  11098  climcau  11109  climrecvg1n  11110  climcaucn  11113  serf0  11114  isumz  11151  fisumss  11154  fsumsplitsn  11172  fsumsplitsnun  11181  isumclim3  11185  isummulc2  11188  fsum2dlemstep  11196  fsumconst  11216  fsumabs  11227  fsumparts  11232  iserabs  11237  fsumiun  11239  isumshft  11252  cvgratnnlemseq  11288  mertenslemub  11296  mertenslemi1  11297  mertenslem2  11298  eftlcl  11383  reeftlcl  11384  eftlub  11385  efsep  11386  effsumlt  11387  eirraplem  11472  2tp1odd  11570  bezoutlemstep  11674  alginv  11717  algfx  11722  cncongr1  11773  qnumdencoprm  11860  qeqnumdivden  11861  unct  11943  epttop  12248  lmss  12404  txlm  12437  lmcn2  12438  cnmpt2c  12448  txswaphmeolem  12478  blfvalps  12543  bdxmet  12659  fsumcncntop  12714  cncfmptc  12740  cncfmpt1f  12742  cdivcncfap  12745  negfcncf  12747  dvidlemap  12818  dvcnp2cntop  12821  dvaddxxbr  12823  dvmulxxbr  12824  dviaddf  12827  dvexp  12833  dvmptaddx  12839  dvmptmulx  12840  dvef  12845  sincn  12847  coscn  12848  nninfsellemeqinf  13201  nninffeq  13205  exmidsbthrlem  13206  cvgcmp2nlemabs  13216