Theorem eqidd 2230

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

Syntax hints:   -> wi 4   = wceq 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  cbvraldva  2774  cbvrexdva  2775  rspcedeq1vd  2917  rspcedeq2vd  2918  nelrdva  3011  opeq2  3859  mpteq1  4169  tfisi  4681  feq23d  5473  f10d  5613  fvmptdv2  5730  elrnrexdm  5780  fmptco  5807  cofmpt  5810  ftpg  5831  fliftfun  5930  fliftval  5934  cbvmpo  6093  fconstmpo  6109  eqfnov2  6122  ovmpod  6142  ovmpodv2  6148  fvmpopr2d  6151  elovmporab  6215  elovmporab1w  6216  ofvalg  6238  ofrval  6239  off  6241  ofres  6243  suppssof1  6246  ofco  6247  caofref  6253  caofid0l  6255  caofid0r  6256  caofid1  6257  caofid2  6258  caofrss  6260  caoftrn  6261  uchoice  6293  rdgivallem  6540  iserd  6721  ixpsnf1o  6898  modom  6987  1domsn  6994  mapxpen  7027  infnninf  7312  ctssexmid  7338  nninfdcinf  7359  nninfwlporlemd  7360  nninfwlporlem  7361  nninfwlpoimlemginf  7364  nninfinfwlpo  7368  ofnegsub  9130  infrenegsupex  9816  fz0to4untppr  10347  fzo0to3tp  10452  modqsubmod  10632  0tonninf  10690  iseqovex  10708  seqvalcd  10711  seq3f1olemqsumkj  10761  seq3id  10775  seq3id2  10776  ccatws1ls  11206  pfxsuffeqwrdeq  11266  wrdind  11290  wrd2ind  11291  ccats1pfxeqbi  11310  s3eq2  11345  resqrexlemp1rp  11554  resqrexlemfp1  11557  resqrex  11574  infxrnegsupex  11811  climcl  11830  clim2  11831  climuni  11841  climeq  11847  2clim  11849  climshftlemg  11850  climabs0  11855  climcn1  11856  climcn2  11857  climge0  11873  climsqz  11883  climsqz2  11884  climcau  11895  climrecvg1n  11896  climcaucn  11899  serf0  11900  isumz  11937  fisumss  11940  fsumsplitsn  11958  fsumsplitsnun  11967  isumclim3  11971  isummulc2  11974  fsum2dlemstep  11982  fsumconst  12002  fsumabs  12013  fsumparts  12018  iserabs  12023  fsumiun  12025  isumshft  12038  cvgratnnlemseq  12074  mertenslemub  12082  mertenslemi1  12083  mertenslem2  12084  prod1dc  12134  fprodssdc  12138  fprodunsn  12152  fprodcl2lem  12153  fprodconst  12168  fprod2dlemstep  12170  fprodsplitsn  12181  eftlcl  12236  reeftlcl  12237  eftlub  12238  efsep  12239  effsumlt  12240  eirraplem  12325  2tp1odd  12432  bezoutlemstep  12555  nninfctlemfo  12598  alginv  12606  algfx  12611  cncongr1  12662  qnumdencoprm  12752  qeqnumdivden  12753  ctiunctal  13049  unct  13050  nninfdclemcl  13056  nninfdclemf  13057  nninfdclemp1  13058  nninfdc  13061  ressbasid  13140  ressressg  13145  prdsex  13339  prdsbaslemss  13344  prdssca  13345  prdsbas  13346  prdsplusg  13347  prdsmulr  13348  imasex  13375  imasbas  13377  imasplusg  13378  imasmulr  13379  qusin  13396  igsumvalx  13459  gsumfzval  13461  gsumpropd  13462  gsumpropd2  13463  gsum0g  13466  gsumval2  13467  issgrp  13473  sgrp1  13481  issgrpd  13482  prdssgrpd  13485  ismndd  13507  mndprop  13511  ress0g  13513  prdsmndd  13518  imasmnd2  13522  insubm  13555  resmhm  13557  resmhm2  13558  resmhm2b  13559  gsumfzz  13565  grpprop  13588  grpsubfvalg  13615  grpressid  13631  grpsubpropdg  13674  prdsgrpd  13679  imasgrp2  13684  imasgrp  13685  imasgrpf1  13686  mulgfvalg  13695  mulgnngsum  13701  mulgpropdg  13738  submmulg  13740  subginv  13755  subgcl  13758  subgsub  13760  releqgg  13794  eqgex  13795  eqgfval  13796  qusgrp  13806  resghm  13834  ablprop  13871  subcmnd  13907  ablressid  13909  gsumfzmptfidmadd  13913  gsumfzconst  13915  gsumfzconstf  13916  gsumfzmhm2  13918  isrng  13934  isrngd  13953  rngressid  13954  imasrng  13956  issrg  13965  srgidmlem  13978  isring  14000  ringass  14016  ringidmlem  14022  ringabl  14032  ringprop  14040  isringd  14041  ring1  14059  ringressid  14063  imasring  14064  opprrng  14077  opprring  14079  opprringbg  14080  opprsubgg  14084  mulgass3  14085  dvdsrcld  14098  dvdsrex  14099  dvdsrcl2  14100  dvdsrid  14101  dvdsrtr  14102  dvdsrneg  14104  dvdsr01  14105  1unit  14108  unitcld  14109  opprunitd  14111  crngunit  14112  unitmulcl  14114  unitgrpbasd  14116  unitgrp  14117  unitabl  14118  unitgrpid  14119  unitsubm  14120  unitlinv  14127  unitrinv  14128  unitnegcl  14131  dvrfvald  14134  dvrvald  14135  dvrcl  14136  unitdvcl  14137  dvrid  14138  dvr1  14139  dvrdir  14144  rdivmuldivd  14145  dvdsrpropdg  14148  unitpropdg  14149  invrpropdg  14150  rhmf1o  14169  rhmdvdsr  14176  elrhmunit  14178  rhmunitinv  14179  issubrng2  14211  subrngpropd  14217  subrgcrng  14226  subrgdvds  14236  subrguss  14237  subrginv  14238  subrgdv  14239  subrgunit  14240  subrgugrp  14241  issubrg2  14242  subrgpropd  14254  aprirr  14284  aprsym  14285  aprcotr  14286  aprap  14287  islmodd  14294  lmodabl  14335  lss1  14363  lsssn0  14371  islss3  14380  lss1d  14384  lssintclm  14385  lsslsp  14430  sralmod  14451  sralmod0g  14452  rlmfn  14454  rlmvalg  14455  rlm0g  14458  rlmvnegg  14466  lidlssbas  14478  islidlm  14480  rnglidlmsgrp  14498  rnglidlrng  14499  qus2idrng  14526  crngridl  14531  quscrng  14534  cnfldui  14590  dvdsrzring  14604  zrhpropd  14627  znzrh  14644  znbas  14645  zncrng  14646  znzrhfo  14649  znf1o  14652  znunit  14660  psrval  14667  psrbaglesuppg  14673  psrbasg  14675  psrplusgg  14679  mplsubgfilemcl  14700  mplplusgg  14704  epttop  14801  lmss  14957  txlm  14990  lmcn2  14991  cnmpt2c  15001  txswaphmeolem  15031  blfvalps  15096  bdxmet  15212  mpomulcn  15277  fsumcncntop  15278  cncfmptc  15307  cncfmpt1f  15309  cdivcncfap  15315  negfcncf  15317  divcncfap  15325  dvidlemap  15402  dvidrelem  15403  dvidsslem  15404  dvcnp2cntop  15410  dvaddxxbr  15412  dvmulxxbr  15413  dviaddf  15416  dvexp  15422  dvmptaddx  15430  dvmptmulx  15431  dvmptfsum  15436  dvef  15438  elply2  15446  elplyr  15451  plyaddlem1  15458  plycolemc  15469  sincn  15480  coscn  15481  lgsdir2lem5  15748  gausslemma2dlem1  15777  lgseisenlem2  15787  lgseisenlem3  15788  lgseisenlem4  15789  lgsquad2lem2  15798  2lgslem1b  15805  2lgslem3b1  15814  2lgslem3c1  15815  2lgsoddprmlem4  15828  2sqlem8  15839  usgredg4  16050  ushgredgedg  16061  ushgredgedgloop  16063  usgrstrrepeen  16066  uspgr1edc  16075  wlk1walkdom  16147  uspgr2wlkeq  16153  uspgr2wlkeqi  16155  clwwlknonmpo  16213  nninfsellemeqinf  16528  nninffeq  16532  nnnninfex  16534  exmidsbthrlem  16536  cvgcmp2nlemabs  16546