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  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  7299  ctssexmid  7325  nninfdcinf  7346  nninfwlporlemd  7347  nninfwlporlem  7348  nninfwlpoimlemginf  7351  nninfinfwlpo  7355  ofnegsub  9117  infrenegsupex  9797  fz0to4untppr  10328  fzo0to3tp  10433  modqsubmod  10612  0tonninf  10670  iseqovex  10688  seqvalcd  10691  seq3f1olemqsumkj  10741  seq3id  10755  seq3id2  10756  ccatws1ls  11181  pfxsuffeqwrdeq  11238  wrdind  11262  wrd2ind  11263  ccats1pfxeqbi  11282  s3eq2  11317  resqrexlemp1rp  11525  resqrexlemfp1  11528  resqrex  11545  infxrnegsupex  11782  climcl  11801  clim2  11802  climuni  11812  climeq  11818  2clim  11820  climshftlemg  11821  climabs0  11826  climcn1  11827  climcn2  11828  climge0  11844  climsqz  11854  climsqz2  11855  climcau  11866  climrecvg1n  11867  climcaucn  11870  serf0  11871  isumz  11908  fisumss  11911  fsumsplitsn  11929  fsumsplitsnun  11938  isumclim3  11942  isummulc2  11945  fsum2dlemstep  11953  fsumconst  11973  fsumabs  11984  fsumparts  11989  iserabs  11994  fsumiun  11996  isumshft  12009  cvgratnnlemseq  12045  mertenslemub  12053  mertenslemi1  12054  mertenslem2  12055  prod1dc  12105  fprodssdc  12109  fprodunsn  12123  fprodcl2lem  12124  fprodconst  12139  fprod2dlemstep  12141  fprodsplitsn  12152  eftlcl  12207  reeftlcl  12208  eftlub  12209  efsep  12210  effsumlt  12211  eirraplem  12296  2tp1odd  12403  bezoutlemstep  12526  nninfctlemfo  12569  alginv  12577  algfx  12582  cncongr1  12633  qnumdencoprm  12723  qeqnumdivden  12724  ctiunctal  13020  unct  13021  nninfdclemcl  13027  nninfdclemf  13028  nninfdclemp1  13029  nninfdc  13032  ressbasid  13111  ressressg  13116  prdsex  13310  prdsbaslemss  13315  prdssca  13316  prdsbas  13317  prdsplusg  13318  prdsmulr  13319  imasex  13346  imasbas  13348  imasplusg  13349  imasmulr  13350  qusin  13367  igsumvalx  13430  gsumfzval  13432  gsumpropd  13433  gsumpropd2  13434  gsum0g  13437  gsumval2  13438  issgrp  13444  sgrp1  13452  issgrpd  13453  prdssgrpd  13456  ismndd  13478  mndprop  13482  ress0g  13484  prdsmndd  13489  imasmnd2  13493  insubm  13526  resmhm  13528  resmhm2  13529  resmhm2b  13530  gsumfzz  13536  grpprop  13559  grpsubfvalg  13586  grpressid  13602  grpsubpropdg  13645  prdsgrpd  13650  imasgrp2  13655  imasgrp  13656  imasgrpf1  13657  mulgfvalg  13666  mulgnngsum  13672  mulgpropdg  13709  submmulg  13711  subginv  13726  subgcl  13729  subgsub  13731  releqgg  13765  eqgex  13766  eqgfval  13767  qusgrp  13777  resghm  13805  ablprop  13842  subcmnd  13878  ablressid  13880  gsumfzmptfidmadd  13884  gsumfzconst  13886  gsumfzconstf  13887  gsumfzmhm2  13889  isrng  13905  isrngd  13924  rngressid  13925  imasrng  13927  issrg  13936  srgidmlem  13949  isring  13971  ringass  13987  ringidmlem  13993  ringabl  14003  ringprop  14011  isringd  14012  ring1  14030  ringressid  14034  imasring  14035  opprrng  14048  opprring  14050  opprringbg  14051  opprsubgg  14055  mulgass3  14056  dvdsrcld  14069  dvdsrex  14070  dvdsrcl2  14071  dvdsrid  14072  dvdsrtr  14073  dvdsrneg  14075  dvdsr01  14076  1unit  14079  unitcld  14080  opprunitd  14082  crngunit  14083  unitmulcl  14085  unitgrpbasd  14087  unitgrp  14088  unitabl  14089  unitgrpid  14090  unitsubm  14091  unitlinv  14098  unitrinv  14099  unitnegcl  14102  dvrfvald  14105  dvrvald  14106  dvrcl  14107  unitdvcl  14108  dvrid  14109  dvr1  14110  dvrdir  14115  rdivmuldivd  14116  dvdsrpropdg  14119  unitpropdg  14120  invrpropdg  14121  rhmf1o  14140  rhmdvdsr  14147  elrhmunit  14149  rhmunitinv  14150  issubrng2  14182  subrngpropd  14188  subrgcrng  14197  subrgdvds  14207  subrguss  14208  subrginv  14209  subrgdv  14210  subrgunit  14211  subrgugrp  14212  issubrg2  14213  subrgpropd  14225  aprirr  14255  aprsym  14256  aprcotr  14257  aprap  14258  islmodd  14265  lmodabl  14306  lss1  14334  lsssn0  14342  islss3  14351  lss1d  14355  lssintclm  14356  lsslsp  14401  sralmod  14422  sralmod0g  14423  rlmfn  14425  rlmvalg  14426  rlm0g  14429  rlmvnegg  14437  lidlssbas  14449  islidlm  14451  rnglidlmsgrp  14469  rnglidlrng  14470  qus2idrng  14497  crngridl  14502  quscrng  14505  cnfldui  14561  dvdsrzring  14575  zrhpropd  14598  znzrh  14615  znbas  14616  zncrng  14617  znzrhfo  14620  znf1o  14623  znunit  14631  psrval  14638  psrbaglesuppg  14644  psrbasg  14646  psrplusgg  14650  mplsubgfilemcl  14671  mplplusgg  14675  epttop  14772  lmss  14928  txlm  14961  lmcn2  14962  cnmpt2c  14972  txswaphmeolem  15002  blfvalps  15067  bdxmet  15183  mpomulcn  15248  fsumcncntop  15249  cncfmptc  15278  cncfmpt1f  15280  cdivcncfap  15286  negfcncf  15288  divcncfap  15296  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvcnp2cntop  15381  dvaddxxbr  15383  dvmulxxbr  15384  dviaddf  15387  dvexp  15393  dvmptaddx  15401  dvmptmulx  15402  dvmptfsum  15407  dvef  15409  elply2  15417  elplyr  15422  plyaddlem1  15429  plycolemc  15440  sincn  15451  coscn  15452  lgsdir2lem5  15719  gausslemma2dlem1  15748  lgseisenlem2  15758  lgseisenlem3  15759  lgseisenlem4  15760  lgsquad2lem2  15769  2lgslem1b  15776  2lgslem3b1  15785  2lgslem3c1  15786  2lgsoddprmlem4  15799  2sqlem8  15810  usgredg4  16021  ushgredgedg  16032  ushgredgedgloop  16034  usgrstrrepeen  16037  wlk1walkdom  16080  uspgr2wlkeq  16086  uspgr2wlkeqi  16088  nninfsellemeqinf  16412  nninffeq  16416  nnnninfex  16418  exmidsbthrlem  16420  cvgcmp2nlemabs  16430