Theorem eqidd 2166

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

Syntax hints:   → wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  cbvraldva  2700  cbvrexdva  2701  rspcedeq1vd  2838  rspcedeq2vd  2839  nelrdva  2932  opeq2  3758  mpteq1  4065  tfisi  4563  feq23d  5332  fvmptdv2  5574  elrnrexdm  5623  fmptco  5650  cofmpt  5653  ftpg  5668  fliftfun  5763  fliftval  5767  cbvmpo  5917  fconstmpo  5933  eqfnov2  5945  ovmpod  5965  ovmpodv2  5971  ofvalg  6058  ofrval  6059  off  6061  ofres  6063  suppssof1  6066  ofco  6067  caofref  6070  caofrss  6073  caoftrn  6074  rdgivallem  6345  iserd  6523  ixpsnf1o  6698  1domsn  6781  mapxpen  6810  infnninf  7084  ctssexmid  7110  infrenegsupex  9528  fz0to4untppr  10055  fzo0to3tp  10150  modqsubmod  10313  0tonninf  10370  iseqovex  10387  seqvalcd  10390  seq3f1olemqsumkj  10429  seq3id  10439  seq3id2  10440  resqrexlemp1rp  10944  resqrexlemfp1  10947  resqrex  10964  infxrnegsupex  11200  climcl  11219  clim2  11220  climuni  11230  climeq  11236  2clim  11238  climshftlemg  11239  climabs0  11244  climcn1  11245  climcn2  11246  climge0  11262  climsqz  11272  climsqz2  11273  climcau  11284  climrecvg1n  11285  climcaucn  11288  serf0  11289  isumz  11326  fisumss  11329  fsumsplitsn  11347  fsumsplitsnun  11356  isumclim3  11360  isummulc2  11363  fsum2dlemstep  11371  fsumconst  11391  fsumabs  11402  fsumparts  11407  iserabs  11412  fsumiun  11414  isumshft  11427  cvgratnnlemseq  11463  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  prod1dc  11523  fprodssdc  11527  fprodunsn  11541  fprodcl2lem  11542  fprodconst  11557  fprod2dlemstep  11559  fprodsplitsn  11570  eftlcl  11625  reeftlcl  11626  eftlub  11627  efsep  11628  effsumlt  11629  eirraplem  11713  2tp1odd  11817  bezoutlemstep  11926  alginv  11975  algfx  11980  cncongr1  12031  qnumdencoprm  12121  qeqnumdivden  12122  ctiunctal  12370  unct  12371  nninfdclemcl  12377  nninfdclemf  12378  nninfdclemp1  12379  nninfdc  12382  epttop  12690  lmss  12846  txlm  12879  lmcn2  12880  cnmpt2c  12890  txswaphmeolem  12920  blfvalps  12985  bdxmet  13101  fsumcncntop  13156  cncfmptc  13182  cncfmpt1f  13184  cdivcncfap  13187  negfcncf  13189  dvidlemap  13260  dvcnp2cntop  13263  dvaddxxbr  13265  dvmulxxbr  13266  dviaddf  13269  dvexp  13275  dvmptaddx  13281  dvmptmulx  13282  dvef  13288  sincn  13290  coscn  13291  lgsdir2lem5  13533  2sqlem8  13559  nninfsellemeqinf  13856  nninffeq  13860  exmidsbthrlem  13861  cvgcmp2nlemabs  13871