Theorem eqidd 2239

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  cbvraldva  2795  cbvrexdva  2796  rspcedeq1vd  2939  rspcedeq2vd  2940  nelrdva  3033  opeq2  3905  mpteq1  4215  tfisi  4734  feq23d  5529  f10d  5675  fvmptdv2  5795  elrnrexdm  5847  fmptco  5874  cofmpt  5877  ftpg  5899  fliftfun  6002  fliftval  6006  cbvmpo  6167  fconstmpo  6183  eqfnov2  6196  ovmpod  6216  ovmpodv2  6222  fvmpopr2d  6225  elovmporab  6289  elovmporab1w  6290  ofvalg  6312  ofrval  6313  off  6315  ofres  6317  suppssof1  6320  ofco  6321  caofref  6327  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  caofrss  6334  caoftrn  6335  uchoice  6371  suppofss1dcl  6504  suppofss2dcl  6505  rdgivallem  6652  iserd  6833  ixpsnf1o  7018  modom  7108  1domsn  7115  mapxpen  7148  ofrfidc  7318  infnninf  7465  ctssexmid  7491  nninfdcinf  7512  nninfwlporlemd  7513  nninfwlporlem  7514  nninfwlpoimlemginf  7517  nninfinfwlpo  7521  ofnegsub  9295  infrenegsupex  10004  fz0to4untppr  10542  fzo0to3tp  10648  modqsubmod  10834  0tonninf  10892  iseqovex  10910  seqvalcd  10913  seq3f1olemqsumkj  10963  seq3id  10977  seq3id2  10978  ccatws1ls  11426  pfxsuffeqwrdeq  11486  wrdind  11510  wrd2ind  11511  ccats1pfxeqbi  11530  s3eq2  11565  resqrexlemp1rp  11788  resqrexlemfp1  11791  resqrex  11808  infxrnegsupex  12048  climcl  12067  clim2  12068  climuni  12078  climeq  12084  2clim  12086  climshftlemg  12087  climabs0  12092  climcn1  12093  climcn2  12094  climge0  12110  climsqz  12120  climsqz2  12121  climcau  12132  climrecvg1n  12133  climcaucn  12136  serf0  12137  fzf1o  12161  isumz  12175  fisumss  12178  fsumsplitsn  12196  fsumsplitsnun  12205  isumclim3  12209  isummulc2  12212  fsum2dlemstep  12220  fsumconst  12240  fsumabs  12251  fsumparts  12256  iserabs  12261  fsumiun  12263  isumshft  12276  cvgratnnlemseq  12312  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  prod1dc  12372  fprodssdc  12376  fprodunsn  12390  fprodcl2lem  12391  fprodconst  12406  fprod2dlemstep  12408  fprodsplitsn  12419  eftlcl  12474  reeftlcl  12475  eftlub  12476  efsep  12477  effsumlt  12478  eirraplem  12563  2tp1odd  12670  bezoutlemstep  12793  nninfctlemfo  12836  alginv  12844  algfx  12849  cncongr1  12900  qnumdencoprm  12992  qeqnumdivden  12993  ballotfilemgun  13320  ballotfilemfg  13321  ballotfilemfrc  13322  ctiunctal  13384  unct  13385  nninfdclemcl  13391  nninfdclemf  13392  nninfdclemp1  13393  nninfdc  13396  ressbasid  13477  ressressg  13482  imasex  13679  imasbas  13681  imasplusg  13682  imasmulr  13683  qusin  13700  gzsumvalx  13762  gzsumfzval  13764  gzsum0  13766  gzsumval2  13767  issgrp  13771  sgrp1  13779  issgrpd  13780  ismndd  13803  mndprop  13807  ress0g  13809  imasmnd2  13812  insubm  13845  resmhm  13847  resmhm2  13848  resmhm2b  13849  grpprop  13876  grpsubfvalg  13903  grpressid  13919  grpsubpropdg  13962  imasgrp2  13966  imasgrp  13967  imasgrpf1  13968  mulgfvalg  13977  mulgnngzsum  13983  mulgpropdg  14020  submmulg  14022  subginv  14037  subgcl  14040  subgsub  14042  releqgg  14076  eqgex  14077  eqgfval  14078  qusgrp  14088  resghm  14116  resscntz  14160  ablprop  14184  cmnsubm  14196  subcmnd  14221  ablressid  14223  gzsumconst  14227  gzsumconstf  14228  gzsummhm2  14230  gzsumsplit0  14232  gzsumshift  14233  gsumvalfi  14236  gzsumgsum  14239  gsumsncmn  14240  gsumzfi  14242  gsummhm2fi  14249  prdsex  14256  prdsbaslemss  14258  prdssca  14259  prdsbas  14260  prdsplusg  14261  prdsmulr  14262  prdssgrpd  14275  prdsmndd  14278  prdsgrpd  14281  isrng  14317  isrngd  14336  rngressid  14337  imasrng  14339  issrg  14353  srgidmlem  14366  isring  14388  ringass  14404  ringidmlem  14411  ringabl  14421  ringprop  14429  isringd  14430  ring1  14448  ringressid  14452  imasring  14453  opprrng  14466  opprring  14468  opprringbg  14469  opprsubgg  14474  mulgass3  14475  dvdsrcld  14488  dvdsrex  14489  dvdsrcl2  14490  dvdsrid  14491  dvdsrtr  14492  dvdsrneg  14494  dvdsr01  14495  1unit  14498  unitcld  14499  opprunitd  14501  crngunit  14502  unitmulcl  14504  unitgrpbasd  14506  unitgrp  14507  unitabl  14508  unitgrpid  14509  unitsubm  14510  unitlinv  14517  unitrinv  14518  unitnegcl  14521  dvrfvald  14524  dvrvald  14525  dvrcl  14526  unitdvcl  14527  dvrid  14528  dvr1  14529  dvrdir  14534  rdivmuldivd  14535  dvdsrpropdg  14538  unitpropdg  14539  invrpropdg  14540  rhmf1o  14559  rhmdvdsr  14566  elrhmunit  14568  rhmunitinv  14569  opprlring  14588  issubrng2  14602  subrngpropd  14608  subrgcrng  14617  subrgdvds  14627  subrguss  14628  subrginv  14629  subrgdv  14630  subrgunit  14631  subrgugrp  14632  issubrg2  14633  subrgpropd  14645  aprunit  14676  aprirr  14679  aprsym  14680  aprcotr  14681  aprap  14682  aprnzr  14683  aprlring  14684  aprprop  14685  opprdrng  14704  islmodd  14713  lmodabl  14755  lss1  14783  lsssn0  14791  islss3  14800  lss1d  14804  lssintclm  14805  lsslsp  14850  sralmod  14871  sralmod0g  14872  rlmfn  14874  rlmvalg  14875  rlm0g  14878  rlmvnegg  14886  lidlssbas  14898  islidlm  14900  rnglidlmsgrp  14918  rnglidlrng  14919  qus2idrng  14946  crngridl  14951  quscrng  14954  cnfldui  15008  dvdsrzring  15022  zrhpropd  15045  znzrh  15062  znbas  15063  zncrng  15064  znzrhfo  15067  znf1o  15070  znunit  15078  isassad  15095  issubassa3  15096  asclfval  15105  ressascl  15123  psrval  15134  psrbaglesuppg  15141  psrbagcon  15146  psrbaglefifi  15147  psrbagconf1o  15149  psrbasg  15150  psrplusgg  15154  psrmulrg  15158  mplsubgfilemcl  15181  mplplusgg  15185  epttop  15282  lmss  15438  txlm  15471  lmcn2  15472  cnmpt2c  15482  txswaphmeolem  15512  blfvalps  15577  bdxmet  15693  mpomulcn  15758  fsumcncntop  15759  cncfmptc  15788  cncfmpt1f  15790  cdivcncfap  15796  negfcncf  15798  divcncfap  15806  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dviaddf  15897  dvexp  15903  dvmptaddx  15911  dvmptmulx  15912  dvmptfsum  15917  dvef  15919  elply2  15927  elplyr  15932  plyaddlem1  15939  plycolemc  15950  sincn  15961  coscn  15962  logfac  16090  chtublem  16256  bposlem6  16277  lgsdir2lem5  16317  gausslemma2dlem1  16346  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgsquad2lem2  16367  2lgslem1b  16374  2lgslem3b1  16383  2lgslem3c1  16384  2lgsoddprmlem4  16397  2sqlem8  16408  usgredg4  16622  ushgredgedg  16633  ushgredgedgloop  16635  usgrstrrepeen  16638  uspgr1edc  16647  wlk1walkdom  16766  uspgr2wlkeq  16772  uspgr2wlkeqi  16774  clwwlknonmpo  16835  iseupth  16854  eupth2lem2dc  16866  konigsberglem2  16896  konigsberglem3  16897  nninfsellemeqinf  17225  nninffeq  17229  nnnninfex  17231  exmidsbthrlem  17233  cvgcmp2nlemabs  17247