Theorem eqidd 2239

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	⊢ (𝜑 → 𝐴 = 𝐴)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2238	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 9	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1402

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 1502  ax-ext 2220

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

This theorem is referenced by:  cbvraldva  2795  cbvrexdva  2796  rspcedeq1vd  2939  rspcedeq2vd  2940  nelrdva  3033  opeq2  3903  mpteq1  4213  tfisi  4732  feq23d  5527  f10d  5673  fvmptdv2  5792  elrnrexdm  5841  fmptco  5868  cofmpt  5871  ftpg  5893  fliftfun  5996  fliftval  6000  cbvmpo  6161  fconstmpo  6177  eqfnov2  6190  ovmpod  6210  ovmpodv2  6216  fvmpopr2d  6219  elovmporab  6283  elovmporab1w  6284  ofvalg  6306  ofrval  6307  off  6309  ofres  6311  suppssof1  6314  ofco  6315  caofref  6321  caofid0l  6323  caofid0r  6324  caofid1  6325  caofid2  6326  caofrss  6328  caoftrn  6329  uchoice  6365  suppofss1dcl  6498  suppofss2dcl  6499  rdgivallem  6646  iserd  6827  ixpsnf1o  7012  modom  7102  1domsn  7109  mapxpen  7142  infnninf  7458  ctssexmid  7484  nninfdcinf  7505  nninfwlporlemd  7506  nninfwlporlem  7507  nninfwlpoimlemginf  7510  nninfinfwlpo  7514  ofnegsub  9286  infrenegsupex  9977  fz0to4untppr  10514  fzo0to3tp  10620  modqsubmod  10802  0tonninf  10860  iseqovex  10878  seqvalcd  10881  seq3f1olemqsumkj  10931  seq3id  10945  seq3id2  10946  ccatws1ls  11393  pfxsuffeqwrdeq  11453  wrdind  11477  wrd2ind  11478  ccats1pfxeqbi  11497  s3eq2  11532  resqrexlemp1rp  11755  resqrexlemfp1  11758  resqrex  11775  infxrnegsupex  12012  climcl  12031  clim2  12032  climuni  12042  climeq  12048  2clim  12050  climshftlemg  12051  climabs0  12056  climcn1  12057  climcn2  12058  climge0  12074  climsqz  12084  climsqz2  12085  climcau  12096  climrecvg1n  12097  climcaucn  12100  serf0  12101  fzf1o  12125  isumz  12139  fisumss  12142  fsumsplitsn  12160  fsumsplitsnun  12169  isumclim3  12173  isummulc2  12176  fsum2dlemstep  12184  fsumconst  12204  fsumabs  12215  fsumparts  12220  iserabs  12225  fsumiun  12227  isumshft  12240  cvgratnnlemseq  12276  mertenslemub  12284  mertenslemi1  12285  mertenslem2  12286  prod1dc  12336  fprodssdc  12340  fprodunsn  12354  fprodcl2lem  12355  fprodconst  12370  fprod2dlemstep  12372  fprodsplitsn  12383  eftlcl  12438  reeftlcl  12439  eftlub  12440  efsep  12441  effsumlt  12442  eirraplem  12527  2tp1odd  12634  bezoutlemstep  12757  nninfctlemfo  12800  alginv  12808  algfx  12813  cncongr1  12864  qnumdencoprm  12954  qeqnumdivden  12955  ballotfilemgun  13251  ballotfilemfg  13252  ballotfilemfrc  13253  ctiunctal  13315  unct  13316  nninfdclemcl  13322  nninfdclemf  13323  nninfdclemp1  13324  nninfdc  13327  ressbasid  13407  ressressg  13412  imasex  13609  imasbas  13611  imasplusg  13612  imasmulr  13613  qusin  13630  gzsumvalx  13692  gzsumfzval  13694  gzsum0  13696  gzsumval2  13697  issgrp  13701  sgrp1  13709  issgrpd  13710  ismndd  13733  mndprop  13737  ress0g  13739  imasmnd2  13742  insubm  13775  resmhm  13777  resmhm2  13778  resmhm2b  13779  grpprop  13806  grpsubfvalg  13833  grpressid  13849  grpsubpropdg  13892  imasgrp2  13896  imasgrp  13897  imasgrpf1  13898  mulgfvalg  13907  mulgnngzsum  13913  mulgpropdg  13950  submmulg  13952  subginv  13967  subgcl  13970  subgsub  13972  releqgg  14006  eqgex  14007  eqgfval  14008  qusgrp  14018  resghm  14046  ablprop  14083  cmnsubm  14095  subcmnd  14120  ablressid  14122  gzsumconst  14126  gzsumconstf  14127  gzsummhm2  14129  gzsumsplit0  14131  gzsumshift  14132  gsumvalfi  14135  gzsumgsum  14138  gsumsncmn  14139  gsumzfi  14141  gsummhm2fi  14148  prdsex  14155  prdsbaslemss  14157  prdssca  14158  prdsbas  14159  prdsplusg  14160  prdsmulr  14161  prdssgrpd  14174  prdsmndd  14177  prdsgrpd  14180  isrng  14216  isrngd  14235  rngressid  14236  imasrng  14238  issrg  14252  srgidmlem  14265  isring  14287  ringass  14303  ringidmlem  14310  ringabl  14320  ringprop  14328  isringd  14329  ring1  14347  ringressid  14351  imasring  14352  opprrng  14365  opprring  14367  opprringbg  14368  opprsubgg  14373  mulgass3  14374  dvdsrcld  14387  dvdsrex  14388  dvdsrcl2  14389  dvdsrid  14390  dvdsrtr  14391  dvdsrneg  14393  dvdsr01  14394  1unit  14397  unitcld  14398  opprunitd  14400  crngunit  14401  unitmulcl  14403  unitgrpbasd  14405  unitgrp  14406  unitabl  14407  unitgrpid  14408  unitsubm  14409  unitlinv  14416  unitrinv  14417  unitnegcl  14420  dvrfvald  14423  dvrvald  14424  dvrcl  14425  unitdvcl  14426  dvrid  14427  dvr1  14428  dvrdir  14433  rdivmuldivd  14434  dvdsrpropdg  14437  unitpropdg  14438  invrpropdg  14439  rhmf1o  14458  rhmdvdsr  14465  elrhmunit  14467  rhmunitinv  14468  opprlring  14487  issubrng2  14501  subrngpropd  14507  subrgcrng  14516  subrgdvds  14526  subrguss  14527  subrginv  14528  subrgdv  14529  subrgunit  14530  subrgugrp  14531  issubrg2  14532  subrgpropd  14544  aprunit  14575  aprirr  14578  aprsym  14579  aprcotr  14580  aprap  14581  aprnzr  14582  aprlring  14583  aprprop  14584  opprdrng  14603  islmodd  14612  lmodabl  14654  lss1  14682  lsssn0  14690  islss3  14699  lss1d  14703  lssintclm  14704  lsslsp  14749  sralmod  14770  sralmod0g  14771  rlmfn  14773  rlmvalg  14774  rlm0g  14777  rlmvnegg  14785  lidlssbas  14797  islidlm  14799  rnglidlmsgrp  14817  rnglidlrng  14818  qus2idrng  14845  crngridl  14850  quscrng  14853  cnfldui  14907  dvdsrzring  14921  zrhpropd  14944  znzrh  14961  znbas  14962  zncrng  14963  znzrhfo  14966  znf1o  14969  znunit  14977  isassad  14994  issubassa3  14995  asclfval  15004  ressascl  15022  psrval  15033  psrbaglesuppg  15040  psrbagcon  15045  psrbagconf1o  15047  psrbasg  15048  psrplusgg  15052  mplsubgfilemcl  15073  mplplusgg  15077  epttop  15174  lmss  15330  txlm  15363  lmcn2  15364  cnmpt2c  15374  txswaphmeolem  15404  blfvalps  15469  bdxmet  15585  mpomulcn  15650  fsumcncntop  15651  cncfmptc  15680  cncfmpt1f  15682  cdivcncfap  15688  negfcncf  15690  divcncfap  15698  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvcnp2cntop  15783  dvaddxxbr  15785  dvmulxxbr  15786  dviaddf  15789  dvexp  15795  dvmptaddx  15803  dvmptmulx  15804  dvmptfsum  15809  dvef  15811  elply2  15819  elplyr  15824  plyaddlem1  15831  plycolemc  15842  sincn  15853  coscn  15854  logfac  15978  lgsdir2lem5  16134  gausslemma2dlem1  16163  lgseisenlem2  16173  lgseisenlem3  16174  lgseisenlem4  16175  lgsquad2lem2  16184  2lgslem1b  16191  2lgslem3b1  16200  2lgslem3c1  16201  2lgsoddprmlem4  16214  2sqlem8  16225  usgredg4  16439  ushgredgedg  16450  ushgredgedgloop  16452  usgrstrrepeen  16455  uspgr1edc  16464  wlk1walkdom  16583  uspgr2wlkeq  16589  uspgr2wlkeqi  16591  clwwlknonmpo  16652  iseupth  16671  eupth2lem2dc  16683  konigsberglem2  16713  konigsberglem3  16714  nninfsellemeqinf  17033  nninffeq  17037  nnnninfex  17039  exmidsbthrlem  17041  cvgcmp2nlemabs  17055