Theorem eqidd 2166

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

Syntax hints:   -> wi 4   = wceq 1343

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 1437  ax-ext 2147

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

This theorem is referenced by:  cbvraldva  2701  cbvrexdva  2702  rspcedeq1vd  2839  rspcedeq2vd  2840  nelrdva  2933  opeq2  3759  mpteq1  4066  tfisi  4564  feq23d  5333  fvmptdv2  5575  elrnrexdm  5624  fmptco  5651  cofmpt  5654  ftpg  5669  fliftfun  5764  fliftval  5768  cbvmpo  5921  fconstmpo  5937  eqfnov2  5949  ovmpod  5969  ovmpodv2  5975  ofvalg  6059  ofrval  6060  off  6062  ofres  6064  suppssof1  6067  ofco  6068  caofref  6071  caofrss  6074  caoftrn  6075  rdgivallem  6349  iserd  6527  ixpsnf1o  6702  1domsn  6785  mapxpen  6814  infnninf  7088  ctssexmid  7114  infrenegsupex  9532  fz0to4untppr  10059  fzo0to3tp  10154  modqsubmod  10317  0tonninf  10374  iseqovex  10391  seqvalcd  10394  seq3f1olemqsumkj  10433  seq3id  10443  seq3id2  10444  resqrexlemp1rp  10948  resqrexlemfp1  10951  resqrex  10968  infxrnegsupex  11204  climcl  11223  clim2  11224  climuni  11234  climeq  11240  2clim  11242  climshftlemg  11243  climabs0  11248  climcn1  11249  climcn2  11250  climge0  11266  climsqz  11276  climsqz2  11277  climcau  11288  climrecvg1n  11289  climcaucn  11292  serf0  11293  isumz  11330  fisumss  11333  fsumsplitsn  11351  fsumsplitsnun  11360  isumclim3  11364  isummulc2  11367  fsum2dlemstep  11375  fsumconst  11395  fsumabs  11406  fsumparts  11411  iserabs  11416  fsumiun  11418  isumshft  11431  cvgratnnlemseq  11467  mertenslemub  11475  mertenslemi1  11476  mertenslem2  11477  prod1dc  11527  fprodssdc  11531  fprodunsn  11545  fprodcl2lem  11546  fprodconst  11561  fprod2dlemstep  11563  fprodsplitsn  11574  eftlcl  11629  reeftlcl  11630  eftlub  11631  efsep  11632  effsumlt  11633  eirraplem  11717  2tp1odd  11821  bezoutlemstep  11930  alginv  11979  algfx  11984  cncongr1  12035  qnumdencoprm  12125  qeqnumdivden  12126  ctiunctal  12374  unct  12375  nninfdclemcl  12381  nninfdclemf  12382  nninfdclemp1  12383  nninfdc  12386  epttop  12730  lmss  12886  txlm  12919  lmcn2  12920  cnmpt2c  12930  txswaphmeolem  12960  blfvalps  13025  bdxmet  13141  fsumcncntop  13196  cncfmptc  13222  cncfmpt1f  13224  cdivcncfap  13227  negfcncf  13229  dvidlemap  13300  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dviaddf  13309  dvexp  13315  dvmptaddx  13321  dvmptmulx  13322  dvef  13328  sincn  13330  coscn  13331  lgsdir2lem5  13573  2sqlem8  13599  nninfsellemeqinf  13896  nninffeq  13900  exmidsbthrlem  13901  cvgcmp2nlemabs  13911