Theorem eqidd 2101

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

Syntax hints:   → wi 4   = wceq 1299

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

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

This theorem is referenced by:  cbvraldva  2618  cbvrexdva  2619  rspcedeq1vd  2752  rspcedeq2vd  2753  nelrdva  2844  opeq2  3653  mpteq1  3952  tfisi  4439  feq23d  5204  fvmptdv2  5442  elrnrexdm  5491  fmptco  5518  cofmpt  5521  ftpg  5536  fliftfun  5629  fliftval  5633  cbvmpo  5782  fconstmpo  5798  eqfnov2  5810  ovmpod  5830  ovmpodv2  5836  fnofval  5923  ofrval  5924  off  5926  ofres  5927  suppssof1  5930  ofco  5931  caofref  5934  caofrss  5937  caoftrn  5938  rdgivallem  6208  iserd  6385  ixpsnf1o  6560  1domsn  6642  mapxpen  6671  ctssexmid  6936  infrenegsupex  9239  fzo0to3tp  9837  modqsubmod  9996  0tonninf  10053  iseqovex  10070  seqvalcd  10073  seq3f1olemqsumkj  10112  seq3id  10122  seq3id2  10123  resqrexlemp1rp  10618  resqrexlemfp1  10621  resqrex  10638  infxrnegsupex  10871  climcl  10890  clim2  10891  climuni  10901  climeq  10907  2clim  10909  climshftlemg  10910  climabs0  10915  climcn1  10916  climcn2  10917  climge0  10933  climsqz  10943  climsqz2  10944  climcau  10955  climrecvg1n  10956  climcaucn  10959  serf0  10960  isumz  10997  fisumss  11000  fsumsplitsn  11018  fsumsplitsnun  11027  isumclim3  11031  isummulc2  11034  fsum2dlemstep  11042  fsumconst  11062  fsumabs  11073  fsumparts  11078  iserabs  11083  fsumiun  11085  isumshft  11098  cvgratnnlemseq  11134  mertenslemub  11142  mertenslemi1  11143  mertenslem2  11144  eftlcl  11192  reeftlcl  11193  eftlub  11194  efsep  11195  effsumlt  11196  eirraplem  11278  2tp1odd  11376  bezoutlemstep  11478  alginv  11521  algfx  11526  cncongr1  11577  qnumdencoprm  11663  qeqnumdivden  11664  epttop  12041  lmss  12196  txlm  12229  lmcn2  12230  cnmpt2c  12240  blfvalps  12313  bdxmet  12429  cncfmptc  12495  cncfmpt1f  12497  cdivcncfap  12499  negfcncf  12501  dvidlemap  12533  nninfsellemeqinf  12796  nninffeq  12800  exmidsbthrlem  12801  cvgcmp2nlemabs  12811