Theorem eqidd 2232

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

Syntax hints:   → wi 4   = wceq 1397

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 1497  ax-ext 2213

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

This theorem is referenced by:  cbvraldva  2776  cbvrexdva  2777  rspcedeq1vd  2919  rspcedeq2vd  2920  nelrdva  3013  opeq2  3863  mpteq1  4173  tfisi  4685  feq23d  5478  f10d  5619  fvmptdv2  5736  elrnrexdm  5786  fmptco  5813  cofmpt  5816  ftpg  5838  fliftfun  5937  fliftval  5941  cbvmpo  6100  fconstmpo  6116  eqfnov2  6129  ovmpod  6149  ovmpodv2  6155  fvmpopr2d  6158  elovmporab  6222  elovmporab1w  6223  ofvalg  6245  ofrval  6246  off  6248  ofres  6250  suppssof1  6253  ofco  6254  caofref  6260  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  caofrss  6267  caoftrn  6268  uchoice  6300  rdgivallem  6547  iserd  6728  ixpsnf1o  6905  modom  6994  1domsn  7001  mapxpen  7034  infnninf  7323  ctssexmid  7349  nninfdcinf  7370  nninfwlporlemd  7371  nninfwlporlem  7372  nninfwlpoimlemginf  7375  nninfinfwlpo  7379  ofnegsub  9142  infrenegsupex  9828  fz0to4untppr  10359  fzo0to3tp  10464  modqsubmod  10644  0tonninf  10702  iseqovex  10720  seqvalcd  10723  seq3f1olemqsumkj  10773  seq3id  10787  seq3id2  10788  ccatws1ls  11219  pfxsuffeqwrdeq  11279  wrdind  11303  wrd2ind  11304  ccats1pfxeqbi  11323  s3eq2  11358  resqrexlemp1rp  11567  resqrexlemfp1  11570  resqrex  11587  infxrnegsupex  11824  climcl  11843  clim2  11844  climuni  11854  climeq  11860  2clim  11862  climshftlemg  11863  climabs0  11868  climcn1  11869  climcn2  11870  climge0  11886  climsqz  11896  climsqz2  11897  climcau  11908  climrecvg1n  11909  climcaucn  11912  serf0  11913  fzf1o  11937  isumz  11951  fisumss  11954  fsumsplitsn  11972  fsumsplitsnun  11981  isumclim3  11985  isummulc2  11988  fsum2dlemstep  11996  fsumconst  12016  fsumabs  12027  fsumparts  12032  iserabs  12037  fsumiun  12039  isumshft  12052  cvgratnnlemseq  12088  mertenslemub  12096  mertenslemi1  12097  mertenslem2  12098  prod1dc  12148  fprodssdc  12152  fprodunsn  12166  fprodcl2lem  12167  fprodconst  12182  fprod2dlemstep  12184  fprodsplitsn  12195  eftlcl  12250  reeftlcl  12251  eftlub  12252  efsep  12253  effsumlt  12254  eirraplem  12339  2tp1odd  12446  bezoutlemstep  12569  nninfctlemfo  12612  alginv  12620  algfx  12625  cncongr1  12676  qnumdencoprm  12766  qeqnumdivden  12767  ctiunctal  13063  unct  13064  nninfdclemcl  13070  nninfdclemf  13071  nninfdclemp1  13072  nninfdc  13075  ressbasid  13154  ressressg  13159  prdsex  13353  prdsbaslemss  13358  prdssca  13359  prdsbas  13360  prdsplusg  13361  prdsmulr  13362  imasex  13389  imasbas  13391  imasplusg  13392  imasmulr  13393  qusin  13410  igsumvalx  13473  gsumfzval  13475  gsumpropd  13476  gsumpropd2  13477  gsum0g  13480  gsumval2  13481  issgrp  13487  sgrp1  13495  issgrpd  13496  prdssgrpd  13499  ismndd  13521  mndprop  13525  ress0g  13527  prdsmndd  13532  imasmnd2  13536  insubm  13569  resmhm  13571  resmhm2  13572  resmhm2b  13573  gsumfzz  13579  grpprop  13602  grpsubfvalg  13629  grpressid  13645  grpsubpropdg  13688  prdsgrpd  13693  imasgrp2  13698  imasgrp  13699  imasgrpf1  13700  mulgfvalg  13709  mulgnngsum  13715  mulgpropdg  13752  submmulg  13754  subginv  13769  subgcl  13772  subgsub  13774  releqgg  13808  eqgex  13809  eqgfval  13810  qusgrp  13820  resghm  13848  ablprop  13885  subcmnd  13921  ablressid  13923  gsumfzmptfidmadd  13927  gsumfzconst  13929  gsumfzconstf  13930  gsumfzmhm2  13932  gsumsplit0  13934  isrng  13949  isrngd  13968  rngressid  13969  imasrng  13971  issrg  13980  srgidmlem  13993  isring  14015  ringass  14031  ringidmlem  14037  ringabl  14047  ringprop  14055  isringd  14056  ring1  14074  ringressid  14078  imasring  14079  opprrng  14092  opprring  14094  opprringbg  14095  opprsubgg  14099  mulgass3  14100  dvdsrcld  14113  dvdsrex  14114  dvdsrcl2  14115  dvdsrid  14116  dvdsrtr  14117  dvdsrneg  14119  dvdsr01  14120  1unit  14123  unitcld  14124  opprunitd  14126  crngunit  14127  unitmulcl  14129  unitgrpbasd  14131  unitgrp  14132  unitabl  14133  unitgrpid  14134  unitsubm  14135  unitlinv  14142  unitrinv  14143  unitnegcl  14146  dvrfvald  14149  dvrvald  14150  dvrcl  14151  unitdvcl  14152  dvrid  14153  dvr1  14154  dvrdir  14159  rdivmuldivd  14160  dvdsrpropdg  14163  unitpropdg  14164  invrpropdg  14165  rhmf1o  14184  rhmdvdsr  14191  elrhmunit  14193  rhmunitinv  14194  issubrng2  14226  subrngpropd  14232  subrgcrng  14241  subrgdvds  14251  subrguss  14252  subrginv  14253  subrgdv  14254  subrgunit  14255  subrgugrp  14256  issubrg2  14257  subrgpropd  14269  aprirr  14299  aprsym  14300  aprcotr  14301  aprap  14302  islmodd  14309  lmodabl  14350  lss1  14378  lsssn0  14386  islss3  14395  lss1d  14399  lssintclm  14400  lsslsp  14445  sralmod  14466  sralmod0g  14467  rlmfn  14469  rlmvalg  14470  rlm0g  14473  rlmvnegg  14481  lidlssbas  14493  islidlm  14495  rnglidlmsgrp  14513  rnglidlrng  14514  qus2idrng  14541  crngridl  14546  quscrng  14549  cnfldui  14605  dvdsrzring  14619  zrhpropd  14642  znzrh  14659  znbas  14660  zncrng  14661  znzrhfo  14664  znf1o  14667  znunit  14675  psrval  14682  psrbaglesuppg  14688  psrbasg  14690  psrplusgg  14694  mplsubgfilemcl  14715  mplplusgg  14719  epttop  14816  lmss  14972  txlm  15005  lmcn2  15006  cnmpt2c  15016  txswaphmeolem  15046  blfvalps  15111  bdxmet  15227  mpomulcn  15292  fsumcncntop  15293  cncfmptc  15322  cncfmpt1f  15324  cdivcncfap  15330  negfcncf  15332  divcncfap  15340  dvidlemap  15417  dvidrelem  15418  dvidsslem  15419  dvcnp2cntop  15425  dvaddxxbr  15427  dvmulxxbr  15428  dviaddf  15431  dvexp  15437  dvmptaddx  15445  dvmptmulx  15446  dvmptfsum  15451  dvef  15453  elply2  15461  elplyr  15466  plyaddlem1  15473  plycolemc  15484  sincn  15495  coscn  15496  lgsdir2lem5  15763  gausslemma2dlem1  15792  lgseisenlem2  15802  lgseisenlem3  15803  lgseisenlem4  15804  lgsquad2lem2  15813  2lgslem1b  15820  2lgslem3b1  15829  2lgslem3c1  15830  2lgsoddprmlem4  15843  2sqlem8  15854  usgredg4  16068  ushgredgedg  16079  ushgredgedgloop  16081  usgrstrrepeen  16084  uspgr1edc  16093  wlk1walkdom  16212  uspgr2wlkeq  16218  uspgr2wlkeqi  16220  clwwlknonmpo  16281  iseupth  16300  eupth2lem2dc  16312  nninfsellemeqinf  16621  nninffeq  16625  nnnninfex  16627  exmidsbthrlem  16629  cvgcmp2nlemabs  16639  gfsumval  16683  gsumgfsumlem  16686  gsumgfsum  16687  gfsumsn  16688