Theorem eqidd 2230

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 2229	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 9	1 ⊢ (𝜑 → 𝐴 = 𝐴)

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  4680  feq23d  5472  f10d  5612  fvmptdv2  5729  elrnrexdm  5779  fmptco  5806  cofmpt  5809  ftpg  5830  fliftfun  5929  fliftval  5933  cbvmpo  6092  fconstmpo  6108  eqfnov2  6121  ovmpod  6141  ovmpodv2  6147  fvmpopr2d  6150  elovmporab  6214  elovmporab1w  6215  ofvalg  6237  ofrval  6238  off  6240  ofres  6242  suppssof1  6245  ofco  6246  caofref  6252  caofid0l  6254  caofid0r  6255  caofid1  6256  caofid2  6257  caofrss  6259  caoftrn  6260  uchoice  6292  rdgivallem  6538  iserd  6719  ixpsnf1o  6896  1domsn  6989  mapxpen  7022  infnninf  7307  ctssexmid  7333  nninfdcinf  7354  nninfwlporlemd  7355  nninfwlporlem  7356  nninfwlpoimlemginf  7359  nninfinfwlpo  7363  ofnegsub  9125  infrenegsupex  9806  fz0to4untppr  10337  fzo0to3tp  10442  modqsubmod  10621  0tonninf  10679  iseqovex  10697  seqvalcd  10700  seq3f1olemqsumkj  10750  seq3id  10764  seq3id2  10765  ccatws1ls  11194  pfxsuffeqwrdeq  11251  wrdind  11275  wrd2ind  11276  ccats1pfxeqbi  11295  s3eq2  11330  resqrexlemp1rp  11538  resqrexlemfp1  11541  resqrex  11558  infxrnegsupex  11795  climcl  11814  clim2  11815  climuni  11825  climeq  11831  2clim  11833  climshftlemg  11834  climabs0  11839  climcn1  11840  climcn2  11841  climge0  11857  climsqz  11867  climsqz2  11868  climcau  11879  climrecvg1n  11880  climcaucn  11883  serf0  11884  isumz  11921  fisumss  11924  fsumsplitsn  11942  fsumsplitsnun  11951  isumclim3  11955  isummulc2  11958  fsum2dlemstep  11966  fsumconst  11986  fsumabs  11997  fsumparts  12002  iserabs  12007  fsumiun  12009  isumshft  12022  cvgratnnlemseq  12058  mertenslemub  12066  mertenslemi1  12067  mertenslem2  12068  prod1dc  12118  fprodssdc  12122  fprodunsn  12136  fprodcl2lem  12137  fprodconst  12152  fprod2dlemstep  12154  fprodsplitsn  12165  eftlcl  12220  reeftlcl  12221  eftlub  12222  efsep  12223  effsumlt  12224  eirraplem  12309  2tp1odd  12416  bezoutlemstep  12539  nninfctlemfo  12582  alginv  12590  algfx  12595  cncongr1  12646  qnumdencoprm  12736  qeqnumdivden  12737  ctiunctal  13033  unct  13034  nninfdclemcl  13040  nninfdclemf  13041  nninfdclemp1  13042  nninfdc  13045  ressbasid  13124  ressressg  13129  prdsex  13323  prdsbaslemss  13328  prdssca  13329  prdsbas  13330  prdsplusg  13331  prdsmulr  13332  imasex  13359  imasbas  13361  imasplusg  13362  imasmulr  13363  qusin  13380  igsumvalx  13443  gsumfzval  13445  gsumpropd  13446  gsumpropd2  13447  gsum0g  13450  gsumval2  13451  issgrp  13457  sgrp1  13465  issgrpd  13466  prdssgrpd  13469  ismndd  13491  mndprop  13495  ress0g  13497  prdsmndd  13502  imasmnd2  13506  insubm  13539  resmhm  13541  resmhm2  13542  resmhm2b  13543  gsumfzz  13549  grpprop  13572  grpsubfvalg  13599  grpressid  13615  grpsubpropdg  13658  prdsgrpd  13663  imasgrp2  13668  imasgrp  13669  imasgrpf1  13670  mulgfvalg  13679  mulgnngsum  13685  mulgpropdg  13722  submmulg  13724  subginv  13739  subgcl  13742  subgsub  13744  releqgg  13778  eqgex  13779  eqgfval  13780  qusgrp  13790  resghm  13818  ablprop  13855  subcmnd  13891  ablressid  13893  gsumfzmptfidmadd  13897  gsumfzconst  13899  gsumfzconstf  13900  gsumfzmhm2  13902  isrng  13918  isrngd  13937  rngressid  13938  imasrng  13940  issrg  13949  srgidmlem  13962  isring  13984  ringass  14000  ringidmlem  14006  ringabl  14016  ringprop  14024  isringd  14025  ring1  14043  ringressid  14047  imasring  14048  opprrng  14061  opprring  14063  opprringbg  14064  opprsubgg  14068  mulgass3  14069  dvdsrcld  14082  dvdsrex  14083  dvdsrcl2  14084  dvdsrid  14085  dvdsrtr  14086  dvdsrneg  14088  dvdsr01  14089  1unit  14092  unitcld  14093  opprunitd  14095  crngunit  14096  unitmulcl  14098  unitgrpbasd  14100  unitgrp  14101  unitabl  14102  unitgrpid  14103  unitsubm  14104  unitlinv  14111  unitrinv  14112  unitnegcl  14115  dvrfvald  14118  dvrvald  14119  dvrcl  14120  unitdvcl  14121  dvrid  14122  dvr1  14123  dvrdir  14128  rdivmuldivd  14129  dvdsrpropdg  14132  unitpropdg  14133  invrpropdg  14134  rhmf1o  14153  rhmdvdsr  14160  elrhmunit  14162  rhmunitinv  14163  issubrng2  14195  subrngpropd  14201  subrgcrng  14210  subrgdvds  14220  subrguss  14221  subrginv  14222  subrgdv  14223  subrgunit  14224  subrgugrp  14225  issubrg2  14226  subrgpropd  14238  aprirr  14268  aprsym  14269  aprcotr  14270  aprap  14271  islmodd  14278  lmodabl  14319  lss1  14347  lsssn0  14355  islss3  14364  lss1d  14368  lssintclm  14369  lsslsp  14414  sralmod  14435  sralmod0g  14436  rlmfn  14438  rlmvalg  14439  rlm0g  14442  rlmvnegg  14450  lidlssbas  14462  islidlm  14464  rnglidlmsgrp  14482  rnglidlrng  14483  qus2idrng  14510  crngridl  14515  quscrng  14518  cnfldui  14574  dvdsrzring  14588  zrhpropd  14611  znzrh  14628  znbas  14629  zncrng  14630  znzrhfo  14633  znf1o  14636  znunit  14644  psrval  14651  psrbaglesuppg  14657  psrbasg  14659  psrplusgg  14663  mplsubgfilemcl  14684  mplplusgg  14688  epttop  14785  lmss  14941  txlm  14974  lmcn2  14975  cnmpt2c  14985  txswaphmeolem  15015  blfvalps  15080  bdxmet  15196  mpomulcn  15261  fsumcncntop  15262  cncfmptc  15291  cncfmpt1f  15293  cdivcncfap  15299  negfcncf  15301  divcncfap  15309  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvcnp2cntop  15394  dvaddxxbr  15396  dvmulxxbr  15397  dviaddf  15400  dvexp  15406  dvmptaddx  15414  dvmptmulx  15415  dvmptfsum  15420  dvef  15422  elply2  15430  elplyr  15435  plyaddlem1  15442  plycolemc  15453  sincn  15464  coscn  15465  lgsdir2lem5  15732  gausslemma2dlem1  15761  lgseisenlem2  15771  lgseisenlem3  15772  lgseisenlem4  15773  lgsquad2lem2  15782  2lgslem1b  15789  2lgslem3b1  15798  2lgslem3c1  15799  2lgsoddprmlem4  15812  2sqlem8  15823  usgredg4  16034  ushgredgedg  16045  ushgredgedgloop  16047  usgrstrrepeen  16050  uspgr1edc  16059  wlk1walkdom  16131  uspgr2wlkeq  16137  uspgr2wlkeqi  16139  nninfsellemeqinf  16496  nninffeq  16500  nnnninfex  16502  exmidsbthrlem  16504  cvgcmp2nlemabs  16514