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  5837  fliftfun  5936  fliftval  5940  cbvmpo  6099  fconstmpo  6115  eqfnov2  6128  ovmpod  6148  ovmpodv2  6154  fvmpopr2d  6157  elovmporab  6221  elovmporab1w  6222  ofvalg  6244  ofrval  6245  off  6247  ofres  6249  suppssof1  6252  ofco  6253  caofref  6259  caofid0l  6261  caofid0r  6262  caofid1  6263  caofid2  6264  caofrss  6266  caoftrn  6267  uchoice  6299  rdgivallem  6546  iserd  6727  ixpsnf1o  6904  modom  6993  1domsn  7000  mapxpen  7033  infnninf  7322  ctssexmid  7348  nninfdcinf  7369  nninfwlporlemd  7370  nninfwlporlem  7371  nninfwlpoimlemginf  7374  nninfinfwlpo  7378  ofnegsub  9141  infrenegsupex  9827  fz0to4untppr  10358  fzo0to3tp  10463  modqsubmod  10643  0tonninf  10701  iseqovex  10719  seqvalcd  10722  seq3f1olemqsumkj  10772  seq3id  10786  seq3id2  10787  ccatws1ls  11218  pfxsuffeqwrdeq  11278  wrdind  11302  wrd2ind  11303  ccats1pfxeqbi  11322  s3eq2  11357  resqrexlemp1rp  11566  resqrexlemfp1  11569  resqrex  11586  infxrnegsupex  11823  climcl  11842  clim2  11843  climuni  11853  climeq  11859  2clim  11861  climshftlemg  11862  climabs0  11867  climcn1  11868  climcn2  11869  climge0  11885  climsqz  11895  climsqz2  11896  climcau  11907  climrecvg1n  11908  climcaucn  11911  serf0  11912  isumz  11949  fisumss  11952  fsumsplitsn  11970  fsumsplitsnun  11979  isumclim3  11983  isummulc2  11986  fsum2dlemstep  11994  fsumconst  12014  fsumabs  12025  fsumparts  12030  iserabs  12035  fsumiun  12037  isumshft  12050  cvgratnnlemseq  12086  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  prod1dc  12146  fprodssdc  12150  fprodunsn  12164  fprodcl2lem  12165  fprodconst  12180  fprod2dlemstep  12182  fprodsplitsn  12193  eftlcl  12248  reeftlcl  12249  eftlub  12250  efsep  12251  effsumlt  12252  eirraplem  12337  2tp1odd  12444  bezoutlemstep  12567  nninfctlemfo  12610  alginv  12618  algfx  12623  cncongr1  12674  qnumdencoprm  12764  qeqnumdivden  12765  ctiunctal  13061  unct  13062  nninfdclemcl  13068  nninfdclemf  13069  nninfdclemp1  13070  nninfdc  13073  ressbasid  13152  ressressg  13157  prdsex  13351  prdsbaslemss  13356  prdssca  13357  prdsbas  13358  prdsplusg  13359  prdsmulr  13360  imasex  13387  imasbas  13389  imasplusg  13390  imasmulr  13391  qusin  13408  igsumvalx  13471  gsumfzval  13473  gsumpropd  13474  gsumpropd2  13475  gsum0g  13478  gsumval2  13479  issgrp  13485  sgrp1  13493  issgrpd  13494  prdssgrpd  13497  ismndd  13519  mndprop  13523  ress0g  13525  prdsmndd  13530  imasmnd2  13534  insubm  13567  resmhm  13569  resmhm2  13570  resmhm2b  13571  gsumfzz  13577  grpprop  13600  grpsubfvalg  13627  grpressid  13643  grpsubpropdg  13686  prdsgrpd  13691  imasgrp2  13696  imasgrp  13697  imasgrpf1  13698  mulgfvalg  13707  mulgnngsum  13713  mulgpropdg  13750  submmulg  13752  subginv  13767  subgcl  13770  subgsub  13772  releqgg  13806  eqgex  13807  eqgfval  13808  qusgrp  13818  resghm  13846  ablprop  13883  subcmnd  13919  ablressid  13921  gsumfzmptfidmadd  13925  gsumfzconst  13927  gsumfzconstf  13928  gsumfzmhm2  13930  isrng  13946  isrngd  13965  rngressid  13966  imasrng  13968  issrg  13977  srgidmlem  13990  isring  14012  ringass  14028  ringidmlem  14034  ringabl  14044  ringprop  14052  isringd  14053  ring1  14071  ringressid  14075  imasring  14076  opprrng  14089  opprring  14091  opprringbg  14092  opprsubgg  14096  mulgass3  14097  dvdsrcld  14110  dvdsrex  14111  dvdsrcl2  14112  dvdsrid  14113  dvdsrtr  14114  dvdsrneg  14116  dvdsr01  14117  1unit  14120  unitcld  14121  opprunitd  14123  crngunit  14124  unitmulcl  14126  unitgrpbasd  14128  unitgrp  14129  unitabl  14130  unitgrpid  14131  unitsubm  14132  unitlinv  14139  unitrinv  14140  unitnegcl  14143  dvrfvald  14146  dvrvald  14147  dvrcl  14148  unitdvcl  14149  dvrid  14150  dvr1  14151  dvrdir  14156  rdivmuldivd  14157  dvdsrpropdg  14160  unitpropdg  14161  invrpropdg  14162  rhmf1o  14181  rhmdvdsr  14188  elrhmunit  14190  rhmunitinv  14191  issubrng2  14223  subrngpropd  14229  subrgcrng  14238  subrgdvds  14248  subrguss  14249  subrginv  14250  subrgdv  14251  subrgunit  14252  subrgugrp  14253  issubrg2  14254  subrgpropd  14266  aprirr  14296  aprsym  14297  aprcotr  14298  aprap  14299  islmodd  14306  lmodabl  14347  lss1  14375  lsssn0  14383  islss3  14392  lss1d  14396  lssintclm  14397  lsslsp  14442  sralmod  14463  sralmod0g  14464  rlmfn  14466  rlmvalg  14467  rlm0g  14470  rlmvnegg  14478  lidlssbas  14490  islidlm  14492  rnglidlmsgrp  14510  rnglidlrng  14511  qus2idrng  14538  crngridl  14543  quscrng  14546  cnfldui  14602  dvdsrzring  14616  zrhpropd  14639  znzrh  14656  znbas  14657  zncrng  14658  znzrhfo  14661  znf1o  14664  znunit  14672  psrval  14679  psrbaglesuppg  14685  psrbasg  14687  psrplusgg  14691  mplsubgfilemcl  14712  mplplusgg  14716  epttop  14813  lmss  14969  txlm  15002  lmcn2  15003  cnmpt2c  15013  txswaphmeolem  15043  blfvalps  15108  bdxmet  15224  mpomulcn  15289  fsumcncntop  15290  cncfmptc  15319  cncfmpt1f  15321  cdivcncfap  15327  negfcncf  15329  divcncfap  15337  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dviaddf  15428  dvexp  15434  dvmptaddx  15442  dvmptmulx  15443  dvmptfsum  15448  dvef  15450  elply2  15458  elplyr  15463  plyaddlem1  15470  plycolemc  15481  sincn  15492  coscn  15493  lgsdir2lem5  15760  gausslemma2dlem1  15789  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgsquad2lem2  15810  2lgslem1b  15817  2lgslem3b1  15826  2lgslem3c1  15827  2lgsoddprmlem4  15840  2sqlem8  15851  usgredg4  16065  ushgredgedg  16076  ushgredgedgloop  16078  usgrstrrepeen  16081  uspgr1edc  16090  wlk1walkdom  16209  uspgr2wlkeq  16215  uspgr2wlkeqi  16217  clwwlknonmpo  16278  iseupth  16297  eupth2lem2dc  16309  nninfsellemeqinf  16618  nninffeq  16622  nnnninfex  16624  exmidsbthrlem  16626  cvgcmp2nlemabs  16636  gfsumval  16680  gsumgfsumlem  16683  gsumgfsum  16684