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  2916  rspcedeq2vd  2917  nelrdva  3010  opeq2  3858  mpteq1  4168  tfisi  4679  feq23d  5469  f10d  5609  fvmptdv2  5726  elrnrexdm  5776  fmptco  5803  cofmpt  5806  ftpg  5827  fliftfun  5926  fliftval  5930  cbvmpo  6089  fconstmpo  6105  eqfnov2  6118  ovmpod  6138  ovmpodv2  6144  fvmpopr2d  6147  elovmporab  6211  elovmporab1w  6212  ofvalg  6234  ofrval  6235  off  6237  ofres  6239  suppssof1  6242  ofco  6243  caofref  6249  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  caofrss  6256  caoftrn  6257  uchoice  6289  rdgivallem  6533  iserd  6714  ixpsnf1o  6891  1domsn  6984  mapxpen  7017  infnninf  7302  ctssexmid  7328  nninfdcinf  7349  nninfwlporlemd  7350  nninfwlporlem  7351  nninfwlpoimlemginf  7354  nninfinfwlpo  7358  ofnegsub  9120  infrenegsupex  9801  fz0to4untppr  10332  fzo0to3tp  10437  modqsubmod  10616  0tonninf  10674  iseqovex  10692  seqvalcd  10695  seq3f1olemqsumkj  10745  seq3id  10759  seq3id2  10760  ccatws1ls  11188  pfxsuffeqwrdeq  11245  wrdind  11269  wrd2ind  11270  ccats1pfxeqbi  11289  s3eq2  11324  resqrexlemp1rp  11532  resqrexlemfp1  11535  resqrex  11552  infxrnegsupex  11789  climcl  11808  clim2  11809  climuni  11819  climeq  11825  2clim  11827  climshftlemg  11828  climabs0  11833  climcn1  11834  climcn2  11835  climge0  11851  climsqz  11861  climsqz2  11862  climcau  11873  climrecvg1n  11874  climcaucn  11877  serf0  11878  isumz  11915  fisumss  11918  fsumsplitsn  11936  fsumsplitsnun  11945  isumclim3  11949  isummulc2  11952  fsum2dlemstep  11960  fsumconst  11980  fsumabs  11991  fsumparts  11996  iserabs  12001  fsumiun  12003  isumshft  12016  cvgratnnlemseq  12052  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  prod1dc  12112  fprodssdc  12116  fprodunsn  12130  fprodcl2lem  12131  fprodconst  12146  fprod2dlemstep  12148  fprodsplitsn  12159  eftlcl  12214  reeftlcl  12215  eftlub  12216  efsep  12217  effsumlt  12218  eirraplem  12303  2tp1odd  12410  bezoutlemstep  12533  nninfctlemfo  12576  alginv  12584  algfx  12589  cncongr1  12640  qnumdencoprm  12730  qeqnumdivden  12731  ctiunctal  13027  unct  13028  nninfdclemcl  13034  nninfdclemf  13035  nninfdclemp1  13036  nninfdc  13039  ressbasid  13118  ressressg  13123  prdsex  13317  prdsbaslemss  13322  prdssca  13323  prdsbas  13324  prdsplusg  13325  prdsmulr  13326  imasex  13353  imasbas  13355  imasplusg  13356  imasmulr  13357  qusin  13374  igsumvalx  13437  gsumfzval  13439  gsumpropd  13440  gsumpropd2  13441  gsum0g  13444  gsumval2  13445  issgrp  13451  sgrp1  13459  issgrpd  13460  prdssgrpd  13463  ismndd  13485  mndprop  13489  ress0g  13491  prdsmndd  13496  imasmnd2  13500  insubm  13533  resmhm  13535  resmhm2  13536  resmhm2b  13537  gsumfzz  13543  grpprop  13566  grpsubfvalg  13593  grpressid  13609  grpsubpropdg  13652  prdsgrpd  13657  imasgrp2  13662  imasgrp  13663  imasgrpf1  13664  mulgfvalg  13673  mulgnngsum  13679  mulgpropdg  13716  submmulg  13718  subginv  13733  subgcl  13736  subgsub  13738  releqgg  13772  eqgex  13773  eqgfval  13774  qusgrp  13784  resghm  13812  ablprop  13849  subcmnd  13885  ablressid  13887  gsumfzmptfidmadd  13891  gsumfzconst  13893  gsumfzconstf  13894  gsumfzmhm2  13896  isrng  13912  isrngd  13931  rngressid  13932  imasrng  13934  issrg  13943  srgidmlem  13956  isring  13978  ringass  13994  ringidmlem  14000  ringabl  14010  ringprop  14018  isringd  14019  ring1  14037  ringressid  14041  imasring  14042  opprrng  14055  opprring  14057  opprringbg  14058  opprsubgg  14062  mulgass3  14063  dvdsrcld  14076  dvdsrex  14077  dvdsrcl2  14078  dvdsrid  14079  dvdsrtr  14080  dvdsrneg  14082  dvdsr01  14083  1unit  14086  unitcld  14087  opprunitd  14089  crngunit  14090  unitmulcl  14092  unitgrpbasd  14094  unitgrp  14095  unitabl  14096  unitgrpid  14097  unitsubm  14098  unitlinv  14105  unitrinv  14106  unitnegcl  14109  dvrfvald  14112  dvrvald  14113  dvrcl  14114  unitdvcl  14115  dvrid  14116  dvr1  14117  dvrdir  14122  rdivmuldivd  14123  dvdsrpropdg  14126  unitpropdg  14127  invrpropdg  14128  rhmf1o  14147  rhmdvdsr  14154  elrhmunit  14156  rhmunitinv  14157  issubrng2  14189  subrngpropd  14195  subrgcrng  14204  subrgdvds  14214  subrguss  14215  subrginv  14216  subrgdv  14217  subrgunit  14218  subrgugrp  14219  issubrg2  14220  subrgpropd  14232  aprirr  14262  aprsym  14263  aprcotr  14264  aprap  14265  islmodd  14272  lmodabl  14313  lss1  14341  lsssn0  14349  islss3  14358  lss1d  14362  lssintclm  14363  lsslsp  14408  sralmod  14429  sralmod0g  14430  rlmfn  14432  rlmvalg  14433  rlm0g  14436  rlmvnegg  14444  lidlssbas  14456  islidlm  14458  rnglidlmsgrp  14476  rnglidlrng  14477  qus2idrng  14504  crngridl  14509  quscrng  14512  cnfldui  14568  dvdsrzring  14582  zrhpropd  14605  znzrh  14622  znbas  14623  zncrng  14624  znzrhfo  14627  znf1o  14630  znunit  14638  psrval  14645  psrbaglesuppg  14651  psrbasg  14653  psrplusgg  14657  mplsubgfilemcl  14678  mplplusgg  14682  epttop  14779  lmss  14935  txlm  14968  lmcn2  14969  cnmpt2c  14979  txswaphmeolem  15009  blfvalps  15074  bdxmet  15190  mpomulcn  15255  fsumcncntop  15256  cncfmptc  15285  cncfmpt1f  15287  cdivcncfap  15293  negfcncf  15295  divcncfap  15303  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dviaddf  15394  dvexp  15400  dvmptaddx  15408  dvmptmulx  15409  dvmptfsum  15414  dvef  15416  elply2  15424  elplyr  15429  plyaddlem1  15436  plycolemc  15447  sincn  15458  coscn  15459  lgsdir2lem5  15726  gausslemma2dlem1  15755  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgsquad2lem2  15776  2lgslem1b  15783  2lgslem3b1  15792  2lgslem3c1  15793  2lgsoddprmlem4  15806  2sqlem8  15817  usgredg4  16028  ushgredgedg  16039  ushgredgedgloop  16041  usgrstrrepeen  16044  wlk1walkdom  16100  uspgr2wlkeq  16106  uspgr2wlkeqi  16108  nninfsellemeqinf  16442  nninffeq  16446  nnnninfex  16448  exmidsbthrlem  16450  cvgcmp2nlemabs  16460