Theorem eqidd 2208

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

Syntax hints:   -> wi 4   = wceq 1373

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 1473  ax-ext 2189

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

This theorem is referenced by:  cbvraldva  2751  cbvrexdva  2752  rspcedeq1vd  2893  rspcedeq2vd  2894  nelrdva  2987  opeq2  3834  mpteq1  4144  tfisi  4653  feq23d  5441  f10d  5579  fvmptdv2  5692  elrnrexdm  5742  fmptco  5769  cofmpt  5772  ftpg  5791  fliftfun  5888  fliftval  5892  cbvmpo  6047  fconstmpo  6063  eqfnov2  6076  ovmpod  6096  ovmpodv2  6102  fvmpopr2d  6105  elovmporab  6169  elovmporab1w  6170  ofvalg  6191  ofrval  6192  off  6194  ofres  6196  suppssof1  6199  ofco  6200  caofref  6206  caofid0l  6208  caofid0r  6209  caofid1  6210  caofid2  6211  caofrss  6213  caoftrn  6214  uchoice  6246  rdgivallem  6490  iserd  6669  ixpsnf1o  6846  1domsn  6939  mapxpen  6970  infnninf  7252  ctssexmid  7278  nninfdcinf  7299  nninfwlporlemd  7300  nninfwlporlem  7301  nninfwlpoimlemginf  7304  nninfinfwlpo  7308  ofnegsub  9070  infrenegsupex  9750  fz0to4untppr  10281  fzo0to3tp  10385  modqsubmod  10564  0tonninf  10622  iseqovex  10640  seqvalcd  10643  seq3f1olemqsumkj  10693  seq3id  10707  seq3id2  10708  ccatws1ls  11132  pfxsuffeqwrdeq  11189  wrdind  11213  wrd2ind  11214  ccats1pfxeqbi  11233  resqrexlemp1rp  11432  resqrexlemfp1  11435  resqrex  11452  infxrnegsupex  11689  climcl  11708  clim2  11709  climuni  11719  climeq  11725  2clim  11727  climshftlemg  11728  climabs0  11733  climcn1  11734  climcn2  11735  climge0  11751  climsqz  11761  climsqz2  11762  climcau  11773  climrecvg1n  11774  climcaucn  11777  serf0  11778  isumz  11815  fisumss  11818  fsumsplitsn  11836  fsumsplitsnun  11845  isumclim3  11849  isummulc2  11852  fsum2dlemstep  11860  fsumconst  11880  fsumabs  11891  fsumparts  11896  iserabs  11901  fsumiun  11903  isumshft  11916  cvgratnnlemseq  11952  mertenslemub  11960  mertenslemi1  11961  mertenslem2  11962  prod1dc  12012  fprodssdc  12016  fprodunsn  12030  fprodcl2lem  12031  fprodconst  12046  fprod2dlemstep  12048  fprodsplitsn  12059  eftlcl  12114  reeftlcl  12115  eftlub  12116  efsep  12117  effsumlt  12118  eirraplem  12203  2tp1odd  12310  bezoutlemstep  12433  nninfctlemfo  12476  alginv  12484  algfx  12489  cncongr1  12540  qnumdencoprm  12630  qeqnumdivden  12631  ctiunctal  12927  unct  12928  nninfdclemcl  12934  nninfdclemf  12935  nninfdclemp1  12936  nninfdc  12939  ressbasid  13017  ressressg  13022  prdsex  13216  prdsbaslemss  13221  prdssca  13222  prdsbas  13223  prdsplusg  13224  prdsmulr  13225  imasex  13252  imasbas  13254  imasplusg  13255  imasmulr  13256  qusin  13273  igsumvalx  13336  gsumfzval  13338  gsumpropd  13339  gsumpropd2  13340  gsum0g  13343  gsumval2  13344  issgrp  13350  sgrp1  13358  issgrpd  13359  prdssgrpd  13362  ismndd  13384  mndprop  13388  ress0g  13390  prdsmndd  13395  imasmnd2  13399  insubm  13432  resmhm  13434  resmhm2  13435  resmhm2b  13436  gsumfzz  13442  grpprop  13465  grpsubfvalg  13492  grpressid  13508  grpsubpropdg  13551  prdsgrpd  13556  imasgrp2  13561  imasgrp  13562  imasgrpf1  13563  mulgfvalg  13572  mulgnngsum  13578  mulgpropdg  13615  submmulg  13617  subginv  13632  subgcl  13635  subgsub  13637  releqgg  13671  eqgex  13672  eqgfval  13673  qusgrp  13683  resghm  13711  ablprop  13748  subcmnd  13784  ablressid  13786  gsumfzmptfidmadd  13790  gsumfzconst  13792  gsumfzconstf  13793  gsumfzmhm2  13795  isrng  13811  isrngd  13830  rngressid  13831  imasrng  13833  issrg  13842  srgidmlem  13855  isring  13877  ringass  13893  ringidmlem  13899  ringabl  13909  ringprop  13917  isringd  13918  ring1  13936  ringressid  13940  imasring  13941  opprrng  13954  opprring  13956  opprringbg  13957  opprsubgg  13961  mulgass3  13962  dvdsrcld  13974  dvdsrex  13975  dvdsrcl2  13976  dvdsrid  13977  dvdsrtr  13978  dvdsrneg  13980  dvdsr01  13981  1unit  13984  unitcld  13985  opprunitd  13987  crngunit  13988  unitmulcl  13990  unitgrpbasd  13992  unitgrp  13993  unitabl  13994  unitgrpid  13995  unitsubm  13996  unitlinv  14003  unitrinv  14004  unitnegcl  14007  dvrfvald  14010  dvrvald  14011  dvrcl  14012  unitdvcl  14013  dvrid  14014  dvr1  14015  dvrdir  14020  rdivmuldivd  14021  dvdsrpropdg  14024  unitpropdg  14025  invrpropdg  14026  rhmf1o  14045  rhmdvdsr  14052  elrhmunit  14054  rhmunitinv  14055  issubrng2  14087  subrngpropd  14093  subrgcrng  14102  subrgdvds  14112  subrguss  14113  subrginv  14114  subrgdv  14115  subrgunit  14116  subrgugrp  14117  issubrg2  14118  subrgpropd  14130  aprirr  14160  aprsym  14161  aprcotr  14162  aprap  14163  islmodd  14170  lmodabl  14211  lss1  14239  lsssn0  14247  islss3  14256  lss1d  14260  lssintclm  14261  lsslsp  14306  sralmod  14327  sralmod0g  14328  rlmfn  14330  rlmvalg  14331  rlm0g  14334  rlmvnegg  14342  lidlssbas  14354  islidlm  14356  rnglidlmsgrp  14374  rnglidlrng  14375  qus2idrng  14402  crngridl  14407  quscrng  14410  cnfldui  14466  dvdsrzring  14480  zrhpropd  14503  znzrh  14520  znbas  14521  zncrng  14522  znzrhfo  14525  znf1o  14528  znunit  14536  psrval  14543  psrbaglesuppg  14549  psrbasg  14551  psrplusgg  14555  mplsubgfilemcl  14576  mplplusgg  14580  epttop  14677  lmss  14833  txlm  14866  lmcn2  14867  cnmpt2c  14877  txswaphmeolem  14907  blfvalps  14972  bdxmet  15088  mpomulcn  15153  fsumcncntop  15154  cncfmptc  15183  cncfmpt1f  15185  cdivcncfap  15191  negfcncf  15193  divcncfap  15201  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvcnp2cntop  15286  dvaddxxbr  15288  dvmulxxbr  15289  dviaddf  15292  dvexp  15298  dvmptaddx  15306  dvmptmulx  15307  dvmptfsum  15312  dvef  15314  elply2  15322  elplyr  15327  plyaddlem1  15334  plycolemc  15345  sincn  15356  coscn  15357  lgsdir2lem5  15624  gausslemma2dlem1  15653  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgsquad2lem2  15674  2lgslem1b  15681  2lgslem3b1  15690  2lgslem3c1  15691  2lgsoddprmlem4  15704  2sqlem8  15715  nninfsellemeqinf  16155  nninffeq  16159  nnnninfex  16161  exmidsbthrlem  16163  cvgcmp2nlemabs  16173