Theorem eqidd 2232

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

Syntax hints:   -> wi 4   = wceq 1397

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 1497  ax-ext 2213

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

This theorem is referenced by:  cbvraldva  2776  cbvrexdva  2777  rspcedeq1vd  2919  rspcedeq2vd  2920  nelrdva  3013  opeq2  3863  mpteq1  4173  tfisi  4685  feq23d  5478  f10d  5619  fvmptdv2  5736  elrnrexdm  5786  fmptco  5813  cofmpt  5816  ftpg  5838  fliftfun  5937  fliftval  5941  cbvmpo  6100  fconstmpo  6116  eqfnov2  6129  ovmpod  6149  ovmpodv2  6155  fvmpopr2d  6158  elovmporab  6222  elovmporab1w  6223  ofvalg  6245  ofrval  6246  off  6248  ofres  6250  suppssof1  6253  ofco  6254  caofref  6260  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  caofrss  6267  caoftrn  6268  uchoice  6300  rdgivallem  6547  iserd  6728  ixpsnf1o  6905  modom  6994  1domsn  7001  mapxpen  7034  infnninf  7323  ctssexmid  7349  nninfdcinf  7370  nninfwlporlemd  7371  nninfwlporlem  7372  nninfwlpoimlemginf  7375  nninfinfwlpo  7379  ofnegsub  9142  infrenegsupex  9828  fz0to4untppr  10359  fzo0to3tp  10465  modqsubmod  10645  0tonninf  10703  iseqovex  10721  seqvalcd  10724  seq3f1olemqsumkj  10774  seq3id  10788  seq3id2  10789  ccatws1ls  11223  pfxsuffeqwrdeq  11283  wrdind  11307  wrd2ind  11308  ccats1pfxeqbi  11327  s3eq2  11362  resqrexlemp1rp  11584  resqrexlemfp1  11587  resqrex  11604  infxrnegsupex  11841  climcl  11860  clim2  11861  climuni  11871  climeq  11877  2clim  11879  climshftlemg  11880  climabs0  11885  climcn1  11886  climcn2  11887  climge0  11903  climsqz  11913  climsqz2  11914  climcau  11925  climrecvg1n  11926  climcaucn  11929  serf0  11930  fzf1o  11954  isumz  11968  fisumss  11971  fsumsplitsn  11989  fsumsplitsnun  11998  isumclim3  12002  isummulc2  12005  fsum2dlemstep  12013  fsumconst  12033  fsumabs  12044  fsumparts  12049  iserabs  12054  fsumiun  12056  isumshft  12069  cvgratnnlemseq  12105  mertenslemub  12113  mertenslemi1  12114  mertenslem2  12115  prod1dc  12165  fprodssdc  12169  fprodunsn  12183  fprodcl2lem  12184  fprodconst  12199  fprod2dlemstep  12201  fprodsplitsn  12212  eftlcl  12267  reeftlcl  12268  eftlub  12269  efsep  12270  effsumlt  12271  eirraplem  12356  2tp1odd  12463  bezoutlemstep  12586  nninfctlemfo  12629  alginv  12637  algfx  12642  cncongr1  12693  qnumdencoprm  12783  qeqnumdivden  12784  ctiunctal  13080  unct  13081  nninfdclemcl  13087  nninfdclemf  13088  nninfdclemp1  13089  nninfdc  13092  ressbasid  13171  ressressg  13176  prdsex  13370  prdsbaslemss  13375  prdssca  13376  prdsbas  13377  prdsplusg  13378  prdsmulr  13379  imasex  13406  imasbas  13408  imasplusg  13409  imasmulr  13410  qusin  13427  igsumvalx  13490  gsumfzval  13492  gsumpropd  13493  gsumpropd2  13494  gsum0g  13497  gsumval2  13498  issgrp  13504  sgrp1  13512  issgrpd  13513  prdssgrpd  13516  ismndd  13538  mndprop  13542  ress0g  13544  prdsmndd  13549  imasmnd2  13553  insubm  13586  resmhm  13588  resmhm2  13589  resmhm2b  13590  gsumfzz  13596  grpprop  13619  grpsubfvalg  13646  grpressid  13662  grpsubpropdg  13705  prdsgrpd  13710  imasgrp2  13715  imasgrp  13716  imasgrpf1  13717  mulgfvalg  13726  mulgnngsum  13732  mulgpropdg  13769  submmulg  13771  subginv  13786  subgcl  13789  subgsub  13791  releqgg  13825  eqgex  13826  eqgfval  13827  qusgrp  13837  resghm  13865  ablprop  13902  subcmnd  13938  ablressid  13940  gsumfzmptfidmadd  13944  gsumfzconst  13946  gsumfzconstf  13947  gsumfzmhm2  13949  gsumsplit0  13951  isrng  13966  isrngd  13985  rngressid  13986  imasrng  13988  issrg  13997  srgidmlem  14010  isring  14032  ringass  14048  ringidmlem  14054  ringabl  14064  ringprop  14072  isringd  14073  ring1  14091  ringressid  14095  imasring  14096  opprrng  14109  opprring  14111  opprringbg  14112  opprsubgg  14116  mulgass3  14117  dvdsrcld  14130  dvdsrex  14131  dvdsrcl2  14132  dvdsrid  14133  dvdsrtr  14134  dvdsrneg  14136  dvdsr01  14137  1unit  14140  unitcld  14141  opprunitd  14143  crngunit  14144  unitmulcl  14146  unitgrpbasd  14148  unitgrp  14149  unitabl  14150  unitgrpid  14151  unitsubm  14152  unitlinv  14159  unitrinv  14160  unitnegcl  14163  dvrfvald  14166  dvrvald  14167  dvrcl  14168  unitdvcl  14169  dvrid  14170  dvr1  14171  dvrdir  14176  rdivmuldivd  14177  dvdsrpropdg  14180  unitpropdg  14181  invrpropdg  14182  rhmf1o  14201  rhmdvdsr  14208  elrhmunit  14210  rhmunitinv  14211  issubrng2  14243  subrngpropd  14249  subrgcrng  14258  subrgdvds  14268  subrguss  14269  subrginv  14270  subrgdv  14271  subrgunit  14272  subrgugrp  14273  issubrg2  14274  subrgpropd  14286  aprirr  14316  aprsym  14317  aprcotr  14318  aprap  14319  islmodd  14326  lmodabl  14367  lss1  14395  lsssn0  14403  islss3  14412  lss1d  14416  lssintclm  14417  lsslsp  14462  sralmod  14483  sralmod0g  14484  rlmfn  14486  rlmvalg  14487  rlm0g  14490  rlmvnegg  14498  lidlssbas  14510  islidlm  14512  rnglidlmsgrp  14530  rnglidlrng  14531  qus2idrng  14558  crngridl  14563  quscrng  14566  cnfldui  14622  dvdsrzring  14636  zrhpropd  14659  znzrh  14676  znbas  14677  zncrng  14678  znzrhfo  14681  znf1o  14684  znunit  14692  psrval  14699  psrbaglesuppg  14705  psrbasg  14707  psrplusgg  14711  mplsubgfilemcl  14732  mplplusgg  14736  epttop  14833  lmss  14989  txlm  15022  lmcn2  15023  cnmpt2c  15033  txswaphmeolem  15063  blfvalps  15128  bdxmet  15244  mpomulcn  15309  fsumcncntop  15310  cncfmptc  15339  cncfmpt1f  15341  cdivcncfap  15347  negfcncf  15349  divcncfap  15357  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dviaddf  15448  dvexp  15454  dvmptaddx  15462  dvmptmulx  15463  dvmptfsum  15468  dvef  15470  elply2  15478  elplyr  15483  plyaddlem1  15490  plycolemc  15501  sincn  15512  coscn  15513  lgsdir2lem5  15780  gausslemma2dlem1  15809  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgsquad2lem2  15830  2lgslem1b  15837  2lgslem3b1  15846  2lgslem3c1  15847  2lgsoddprmlem4  15860  2sqlem8  15871  usgredg4  16085  ushgredgedg  16096  ushgredgedgloop  16098  usgrstrrepeen  16101  uspgr1edc  16110  wlk1walkdom  16229  uspgr2wlkeq  16235  uspgr2wlkeqi  16237  clwwlknonmpo  16298  iseupth  16317  eupth2lem2dc  16329  konigsberglem2  16359  konigsberglem3  16360  nninfsellemeqinf  16669  nninffeq  16673  nnnninfex  16675  exmidsbthrlem  16677  cvgcmp2nlemabs  16687  gfsumval  16732  gsumgfsumlem  16735  gsumgfsum  16736  gfsumsn  16737