Theorem eqidd 2197

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

Syntax hints:   → wi 4   = wceq 1364

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 1463  ax-ext 2178

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

This theorem is referenced by:  cbvraldva  2738  cbvrexdva  2739  rspcedeq1vd  2877  rspcedeq2vd  2878  nelrdva  2971  opeq2  3810  mpteq1  4118  tfisi  4624  feq23d  5406  fvmptdv2  5654  elrnrexdm  5704  fmptco  5731  cofmpt  5734  ftpg  5749  fliftfun  5846  fliftval  5850  cbvmpo  6005  fconstmpo  6021  eqfnov2  6034  ovmpod  6054  ovmpodv2  6060  fvmpopr2d  6063  elovmporab  6127  elovmporab1w  6128  ofvalg  6149  ofrval  6150  off  6152  ofres  6154  suppssof1  6157  ofco  6158  caofref  6164  caofid0l  6166  caofid0r  6167  caofid1  6168  caofid2  6169  caofrss  6171  caoftrn  6172  uchoice  6204  rdgivallem  6448  iserd  6627  ixpsnf1o  6804  1domsn  6887  mapxpen  6918  infnninf  7199  ctssexmid  7225  nninfdcinf  7246  nninfwlporlemd  7247  nninfwlporlem  7248  nninfwlpoimlemginf  7251  nninfinfwlpo  7255  ofnegsub  9008  infrenegsupex  9687  fz0to4untppr  10218  fzo0to3tp  10314  modqsubmod  10493  0tonninf  10551  iseqovex  10569  seqvalcd  10572  seq3f1olemqsumkj  10622  seq3id  10636  seq3id2  10637  resqrexlemp1rp  11190  resqrexlemfp1  11193  resqrex  11210  infxrnegsupex  11447  climcl  11466  clim2  11467  climuni  11477  climeq  11483  2clim  11485  climshftlemg  11486  climabs0  11491  climcn1  11492  climcn2  11493  climge0  11509  climsqz  11519  climsqz2  11520  climcau  11531  climrecvg1n  11532  climcaucn  11535  serf0  11536  isumz  11573  fisumss  11576  fsumsplitsn  11594  fsumsplitsnun  11603  isumclim3  11607  isummulc2  11610  fsum2dlemstep  11618  fsumconst  11638  fsumabs  11649  fsumparts  11654  iserabs  11659  fsumiun  11661  isumshft  11674  cvgratnnlemseq  11710  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  prod1dc  11770  fprodssdc  11774  fprodunsn  11788  fprodcl2lem  11789  fprodconst  11804  fprod2dlemstep  11806  fprodsplitsn  11817  eftlcl  11872  reeftlcl  11873  eftlub  11874  efsep  11875  effsumlt  11876  eirraplem  11961  2tp1odd  12068  bezoutlemstep  12191  nninfctlemfo  12234  alginv  12242  algfx  12247  cncongr1  12298  qnumdencoprm  12388  qeqnumdivden  12389  ctiunctal  12685  unct  12686  nninfdclemcl  12692  nninfdclemf  12693  nninfdclemp1  12694  nninfdc  12697  ressbasid  12775  ressressg  12780  prdsex  12973  prdsbaslemss  12978  prdssca  12979  prdsbas  12980  prdsplusg  12981  prdsmulr  12982  imasex  13009  imasbas  13011  imasplusg  13012  imasmulr  13013  qusin  13030  igsumvalx  13093  gsumfzval  13095  gsumpropd  13096  gsumpropd2  13097  gsum0g  13100  gsumval2  13101  issgrp  13107  sgrp1  13115  issgrpd  13116  prdssgrpd  13119  ismndd  13141  mndprop  13145  ress0g  13147  prdsmndd  13152  imasmnd2  13156  insubm  13189  resmhm  13191  resmhm2  13192  resmhm2b  13193  gsumfzz  13199  grpprop  13222  grpsubfvalg  13249  grpressid  13265  grpsubpropdg  13308  prdsgrpd  13313  imasgrp2  13318  imasgrp  13319  imasgrpf1  13320  mulgfvalg  13329  mulgnngsum  13335  mulgpropdg  13372  submmulg  13374  subginv  13389  subgcl  13392  subgsub  13394  releqgg  13428  eqgex  13429  eqgfval  13430  qusgrp  13440  resghm  13468  ablprop  13505  subcmnd  13541  ablressid  13543  gsumfzmptfidmadd  13547  gsumfzconst  13549  gsumfzconstf  13550  gsumfzmhm2  13552  isrng  13568  isrngd  13587  rngressid  13588  imasrng  13590  issrg  13599  srgidmlem  13612  isring  13634  ringass  13650  ringidmlem  13656  ringabl  13666  ringprop  13674  isringd  13675  ring1  13693  ringressid  13697  imasring  13698  opprrng  13711  opprring  13713  opprringbg  13714  opprsubgg  13718  mulgass3  13719  dvdsrcld  13731  dvdsrex  13732  dvdsrcl2  13733  dvdsrid  13734  dvdsrtr  13735  dvdsrneg  13737  dvdsr01  13738  1unit  13741  unitcld  13742  opprunitd  13744  crngunit  13745  unitmulcl  13747  unitgrpbasd  13749  unitgrp  13750  unitabl  13751  unitgrpid  13752  unitsubm  13753  unitlinv  13760  unitrinv  13761  unitnegcl  13764  dvrfvald  13767  dvrvald  13768  dvrcl  13769  unitdvcl  13770  dvrid  13771  dvr1  13772  dvrdir  13777  rdivmuldivd  13778  dvdsrpropdg  13781  unitpropdg  13782  invrpropdg  13783  rhmf1o  13802  rhmdvdsr  13809  elrhmunit  13811  rhmunitinv  13812  issubrng2  13844  subrngpropd  13850  subrgcrng  13859  subrgdvds  13869  subrguss  13870  subrginv  13871  subrgdv  13872  subrgunit  13873  subrgugrp  13874  issubrg2  13875  subrgpropd  13887  aprirr  13917  aprsym  13918  aprcotr  13919  aprap  13920  islmodd  13927  lmodabl  13968  lss1  13996  lsssn0  14004  islss3  14013  lss1d  14017  lssintclm  14018  lsslsp  14063  sralmod  14084  sralmod0g  14085  rlmfn  14087  rlmvalg  14088  rlm0g  14091  rlmvnegg  14099  lidlssbas  14111  islidlm  14113  rnglidlmsgrp  14131  rnglidlrng  14132  qus2idrng  14159  crngridl  14164  quscrng  14167  cnfldui  14223  dvdsrzring  14237  zrhpropd  14260  znzrh  14277  znbas  14278  zncrng  14279  znzrhfo  14282  znf1o  14285  znunit  14293  psrval  14300  psrbaglesuppg  14306  psrbasg  14308  psrplusgg  14312  mplsubgfilemcl  14333  mplplusgg  14337  epttop  14434  lmss  14590  txlm  14623  lmcn2  14624  cnmpt2c  14634  txswaphmeolem  14664  blfvalps  14729  bdxmet  14845  mpomulcn  14910  fsumcncntop  14911  cncfmptc  14940  cncfmpt1f  14942  cdivcncfap  14948  negfcncf  14950  divcncfap  14958  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvcnp2cntop  15043  dvaddxxbr  15045  dvmulxxbr  15046  dviaddf  15049  dvexp  15055  dvmptaddx  15063  dvmptmulx  15064  dvmptfsum  15069  dvef  15071  elply2  15079  elplyr  15084  plyaddlem1  15091  plycolemc  15102  sincn  15113  coscn  15114  lgsdir2lem5  15381  gausslemma2dlem1  15410  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgsquad2lem2  15431  2lgslem1b  15438  2lgslem3b1  15447  2lgslem3c1  15448  2lgsoddprmlem4  15461  2sqlem8  15472  nninfsellemeqinf  15771  nninffeq  15775  nnnninfex  15777  exmidsbthrlem  15779  cvgcmp2nlemabs  15789