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  3809  mpteq1  4117  tfisi  4623  feq23d  5403  fvmptdv2  5651  elrnrexdm  5701  fmptco  5728  cofmpt  5731  ftpg  5746  fliftfun  5843  fliftval  5847  cbvmpo  6001  fconstmpo  6017  eqfnov2  6030  ovmpod  6050  ovmpodv2  6056  fvmpopr2d  6059  elovmporab  6123  elovmporab1w  6124  ofvalg  6145  ofrval  6146  off  6148  ofres  6150  suppssof1  6153  ofco  6154  caofref  6159  caofrss  6162  caoftrn  6163  uchoice  6195  rdgivallem  6439  iserd  6618  ixpsnf1o  6795  1domsn  6878  mapxpen  6909  infnninf  7190  ctssexmid  7216  nninfdcinf  7237  nninfwlporlemd  7238  nninfwlporlem  7239  nninfwlpoimlemginf  7242  ofnegsub  8989  infrenegsupex  9668  fz0to4untppr  10199  fzo0to3tp  10295  modqsubmod  10474  0tonninf  10532  iseqovex  10550  seqvalcd  10553  seq3f1olemqsumkj  10603  seq3id  10617  seq3id2  10618  resqrexlemp1rp  11171  resqrexlemfp1  11174  resqrex  11191  infxrnegsupex  11428  climcl  11447  clim2  11448  climuni  11458  climeq  11464  2clim  11466  climshftlemg  11467  climabs0  11472  climcn1  11473  climcn2  11474  climge0  11490  climsqz  11500  climsqz2  11501  climcau  11512  climrecvg1n  11513  climcaucn  11516  serf0  11517  isumz  11554  fisumss  11557  fsumsplitsn  11575  fsumsplitsnun  11584  isumclim3  11588  isummulc2  11591  fsum2dlemstep  11599  fsumconst  11619  fsumabs  11630  fsumparts  11635  iserabs  11640  fsumiun  11642  isumshft  11655  cvgratnnlemseq  11691  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  prod1dc  11751  fprodssdc  11755  fprodunsn  11769  fprodcl2lem  11770  fprodconst  11785  fprod2dlemstep  11787  fprodsplitsn  11798  eftlcl  11853  reeftlcl  11854  eftlub  11855  efsep  11856  effsumlt  11857  eirraplem  11942  2tp1odd  12049  bezoutlemstep  12164  nninfctlemfo  12207  alginv  12215  algfx  12220  cncongr1  12271  qnumdencoprm  12361  qeqnumdivden  12362  ctiunctal  12658  unct  12659  nninfdclemcl  12665  nninfdclemf  12666  nninfdclemp1  12667  nninfdc  12670  ressbasid  12748  ressressg  12753  prdsex  12940  imasex  12948  imasbas  12950  imasplusg  12951  imasmulr  12952  qusin  12969  igsumvalx  13032  gsumfzval  13034  gsumpropd  13035  gsumpropd2  13036  gsum0g  13039  gsumval2  13040  issgrp  13046  sgrp1  13054  issgrpd  13055  ismndd  13078  mndprop  13082  ress0g  13084  insubm  13117  resmhm  13119  resmhm2  13120  resmhm2b  13121  gsumfzz  13127  grpprop  13150  grpsubfvalg  13177  grpressid  13193  grpsubpropdg  13236  imasgrp2  13240  imasgrp  13241  imasgrpf1  13242  mulgfvalg  13251  mulgnngsum  13257  mulgpropdg  13294  submmulg  13296  subginv  13311  subgcl  13314  subgsub  13316  releqgg  13350  eqgex  13351  eqgfval  13352  qusgrp  13362  resghm  13390  ablprop  13427  subcmnd  13463  ablressid  13465  gsumfzmptfidmadd  13469  gsumfzconst  13471  gsumfzconstf  13472  gsumfzmhm2  13474  isrng  13490  isrngd  13509  rngressid  13510  imasrng  13512  issrg  13521  srgidmlem  13534  isring  13556  ringass  13572  ringidmlem  13578  ringabl  13588  ringprop  13596  isringd  13597  ring1  13615  ringressid  13619  imasring  13620  opprrng  13633  opprring  13635  opprringbg  13636  opprsubgg  13640  mulgass3  13641  dvdsrcld  13653  dvdsrex  13654  dvdsrcl2  13655  dvdsrid  13656  dvdsrtr  13657  dvdsrneg  13659  dvdsr01  13660  1unit  13663  unitcld  13664  opprunitd  13666  crngunit  13667  unitmulcl  13669  unitgrpbasd  13671  unitgrp  13672  unitabl  13673  unitgrpid  13674  unitsubm  13675  unitlinv  13682  unitrinv  13683  unitnegcl  13686  dvrfvald  13689  dvrvald  13690  dvrcl  13691  unitdvcl  13692  dvrid  13693  dvr1  13694  dvrdir  13699  rdivmuldivd  13700  dvdsrpropdg  13703  unitpropdg  13704  invrpropdg  13705  rhmf1o  13724  rhmdvdsr  13731  elrhmunit  13733  rhmunitinv  13734  issubrng2  13766  subrngpropd  13772  subrgcrng  13781  subrgdvds  13791  subrguss  13792  subrginv  13793  subrgdv  13794  subrgunit  13795  subrgugrp  13796  issubrg2  13797  subrgpropd  13809  aprirr  13839  aprsym  13840  aprcotr  13841  aprap  13842  islmodd  13849  lmodabl  13890  lss1  13918  lsssn0  13926  islss3  13935  lss1d  13939  lssintclm  13940  lsslsp  13985  sralmod  14006  sralmod0g  14007  rlmfn  14009  rlmvalg  14010  rlm0g  14013  rlmvnegg  14021  lidlssbas  14033  islidlm  14035  rnglidlmsgrp  14053  rnglidlrng  14054  qus2idrng  14081  crngridl  14086  quscrng  14089  cnfldui  14145  dvdsrzring  14159  zrhpropd  14182  znzrh  14199  znbas  14200  zncrng  14201  znzrhfo  14204  znf1o  14207  znunit  14215  psrval  14220  psrbaglesuppg  14226  psrbasg  14227  psrplusgg  14230  epttop  14326  lmss  14482  txlm  14515  lmcn2  14516  cnmpt2c  14526  txswaphmeolem  14556  blfvalps  14621  bdxmet  14737  mpomulcn  14802  fsumcncntop  14803  cncfmptc  14832  cncfmpt1f  14834  cdivcncfap  14840  negfcncf  14842  divcncfap  14850  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dviaddf  14941  dvexp  14947  dvmptaddx  14955  dvmptmulx  14956  dvmptfsum  14961  dvef  14963  elply2  14971  elplyr  14976  plyaddlem1  14983  plycolemc  14994  sincn  15005  coscn  15006  lgsdir2lem5  15273  gausslemma2dlem1  15302  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgsquad2lem2  15323  2lgslem1b  15330  2lgslem3b1  15339  2lgslem3c1  15340  2lgsoddprmlem4  15353  2sqlem8  15364  nninfsellemeqinf  15660  nninffeq  15664  exmidsbthrlem  15666  cvgcmp2nlemabs  15676