Theorem eqidd 2141

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

Syntax hints:   → wi 4   = wceq 1332

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 1426  ax-ext 2122

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

This theorem is referenced by:  cbvraldva  2666  cbvrexdva  2667  rspcedeq1vd  2802  rspcedeq2vd  2803  nelrdva  2895  opeq2  3714  mpteq1  4020  tfisi  4509  feq23d  5276  fvmptdv2  5518  elrnrexdm  5567  fmptco  5594  cofmpt  5597  ftpg  5612  fliftfun  5705  fliftval  5709  cbvmpo  5858  fconstmpo  5874  eqfnov2  5886  ovmpod  5906  ovmpodv2  5912  ofvalg  5999  ofrval  6000  off  6002  ofres  6004  suppssof1  6007  ofco  6008  caofref  6011  caofrss  6014  caoftrn  6015  rdgivallem  6286  iserd  6463  ixpsnf1o  6638  1domsn  6721  mapxpen  6750  ctssexmid  7032  infrenegsupex  9416  fzo0to3tp  10027  modqsubmod  10186  0tonninf  10243  iseqovex  10260  seqvalcd  10263  seq3f1olemqsumkj  10302  seq3id  10312  seq3id2  10313  resqrexlemp1rp  10810  resqrexlemfp1  10813  resqrex  10830  infxrnegsupex  11064  climcl  11083  clim2  11084  climuni  11094  climeq  11100  2clim  11102  climshftlemg  11103  climabs0  11108  climcn1  11109  climcn2  11110  climge0  11126  climsqz  11136  climsqz2  11137  climcau  11148  climrecvg1n  11149  climcaucn  11152  serf0  11153  isumz  11190  fisumss  11193  fsumsplitsn  11211  fsumsplitsnun  11220  isumclim3  11224  isummulc2  11227  fsum2dlemstep  11235  fsumconst  11255  fsumabs  11266  fsumparts  11271  iserabs  11276  fsumiun  11278  isumshft  11291  cvgratnnlemseq  11327  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  eftlcl  11431  reeftlcl  11432  eftlub  11433  efsep  11434  effsumlt  11435  eirraplem  11519  2tp1odd  11617  bezoutlemstep  11721  alginv  11764  algfx  11769  cncongr1  11820  qnumdencoprm  11907  qeqnumdivden  11908  ctiunctal  11990  unct  11991  epttop  12298  lmss  12454  txlm  12487  lmcn2  12488  cnmpt2c  12498  txswaphmeolem  12528  blfvalps  12593  bdxmet  12709  fsumcncntop  12764  cncfmptc  12790  cncfmpt1f  12792  cdivcncfap  12795  negfcncf  12797  dvidlemap  12868  dvcnp2cntop  12871  dvaddxxbr  12873  dvmulxxbr  12874  dviaddf  12877  dvexp  12883  dvmptaddx  12889  dvmptmulx  12890  dvef  12896  sincn  12898  coscn  12899  nninfsellemeqinf  13387  nninffeq  13391  exmidsbthrlem  13392  cvgcmp2nlemabs  13402