Theorem eqidd 2165

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

Syntax hints:   -> wi 4   = wceq 1342

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 1436  ax-ext 2146

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

This theorem is referenced by:  cbvraldva  2698  cbvrexdva  2699  rspcedeq1vd  2834  rspcedeq2vd  2835  nelrdva  2928  opeq2  3753  mpteq1  4060  tfisi  4558  feq23d  5327  fvmptdv2  5569  elrnrexdm  5618  fmptco  5645  cofmpt  5648  ftpg  5663  fliftfun  5758  fliftval  5762  cbvmpo  5912  fconstmpo  5928  eqfnov2  5940  ovmpod  5960  ovmpodv2  5966  ofvalg  6053  ofrval  6054  off  6056  ofres  6058  suppssof1  6061  ofco  6062  caofref  6065  caofrss  6068  caoftrn  6069  rdgivallem  6340  iserd  6518  ixpsnf1o  6693  1domsn  6776  mapxpen  6805  infnninf  7079  ctssexmid  7105  infrenegsupex  9523  fz0to4untppr  10049  fzo0to3tp  10144  modqsubmod  10307  0tonninf  10364  iseqovex  10381  seqvalcd  10384  seq3f1olemqsumkj  10423  seq3id  10433  seq3id2  10434  resqrexlemp1rp  10934  resqrexlemfp1  10937  resqrex  10954  infxrnegsupex  11190  climcl  11209  clim2  11210  climuni  11220  climeq  11226  2clim  11228  climshftlemg  11229  climabs0  11234  climcn1  11235  climcn2  11236  climge0  11252  climsqz  11262  climsqz2  11263  climcau  11274  climrecvg1n  11275  climcaucn  11278  serf0  11279  isumz  11316  fisumss  11319  fsumsplitsn  11337  fsumsplitsnun  11346  isumclim3  11350  isummulc2  11353  fsum2dlemstep  11361  fsumconst  11381  fsumabs  11392  fsumparts  11397  iserabs  11402  fsumiun  11404  isumshft  11417  cvgratnnlemseq  11453  mertenslemub  11461  mertenslemi1  11462  mertenslem2  11463  prod1dc  11513  fprodssdc  11517  fprodunsn  11531  fprodcl2lem  11532  fprodconst  11547  fprod2dlemstep  11549  fprodsplitsn  11560  eftlcl  11615  reeftlcl  11616  eftlub  11617  efsep  11618  effsumlt  11619  eirraplem  11703  2tp1odd  11806  bezoutlemstep  11915  alginv  11958  algfx  11963  cncongr1  12014  qnumdencoprm  12102  qeqnumdivden  12103  ctiunctal  12311  unct  12312  nninfdclemcl  12320  nninfdclemf  12321  nninfdclemp1  12322  nninfdc  12325  epttop  12631  lmss  12787  txlm  12820  lmcn2  12821  cnmpt2c  12831  txswaphmeolem  12861  blfvalps  12926  bdxmet  13042  fsumcncntop  13097  cncfmptc  13123  cncfmpt1f  13125  cdivcncfap  13128  negfcncf  13130  dvidlemap  13201  dvcnp2cntop  13204  dvaddxxbr  13206  dvmulxxbr  13207  dviaddf  13210  dvexp  13216  dvmptaddx  13222  dvmptmulx  13223  dvef  13229  sincn  13231  coscn  13232  nninfsellemeqinf  13730  nninffeq  13734  exmidsbthrlem  13735  cvgcmp2nlemabs  13745