Theorem eqidd 2140

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

Syntax hints:   → wi 4   = wceq 1331

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 1425  ax-ext 2121

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

This theorem is referenced by:  cbvraldva  2663  cbvrexdva  2664  rspcedeq1vd  2798  rspcedeq2vd  2799  nelrdva  2891  opeq2  3706  mpteq1  4012  tfisi  4501  feq23d  5268  fvmptdv2  5510  elrnrexdm  5559  fmptco  5586  cofmpt  5589  ftpg  5604  fliftfun  5697  fliftval  5701  cbvmpo  5850  fconstmpo  5866  eqfnov2  5878  ovmpod  5898  ovmpodv2  5904  ofvalg  5991  ofrval  5992  off  5994  ofres  5996  suppssof1  5999  ofco  6000  caofref  6003  caofrss  6006  caoftrn  6007  rdgivallem  6278  iserd  6455  ixpsnf1o  6630  1domsn  6713  mapxpen  6742  ctssexmid  7024  infrenegsupex  9389  fzo0to3tp  9996  modqsubmod  10155  0tonninf  10212  iseqovex  10229  seqvalcd  10232  seq3f1olemqsumkj  10271  seq3id  10281  seq3id2  10282  resqrexlemp1rp  10778  resqrexlemfp1  10781  resqrex  10798  infxrnegsupex  11032  climcl  11051  clim2  11052  climuni  11062  climeq  11068  2clim  11070  climshftlemg  11071  climabs0  11076  climcn1  11077  climcn2  11078  climge0  11094  climsqz  11104  climsqz2  11105  climcau  11116  climrecvg1n  11117  climcaucn  11120  serf0  11121  isumz  11158  fisumss  11161  fsumsplitsn  11179  fsumsplitsnun  11188  isumclim3  11192  isummulc2  11195  fsum2dlemstep  11203  fsumconst  11223  fsumabs  11234  fsumparts  11239  iserabs  11244  fsumiun  11246  isumshft  11259  cvgratnnlemseq  11295  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  eftlcl  11394  reeftlcl  11395  eftlub  11396  efsep  11397  effsumlt  11398  eirraplem  11483  2tp1odd  11581  bezoutlemstep  11685  alginv  11728  algfx  11733  cncongr1  11784  qnumdencoprm  11871  qeqnumdivden  11872  unct  11954  epttop  12259  lmss  12415  txlm  12448  lmcn2  12449  cnmpt2c  12459  txswaphmeolem  12489  blfvalps  12554  bdxmet  12670  fsumcncntop  12725  cncfmptc  12751  cncfmpt1f  12753  cdivcncfap  12756  negfcncf  12758  dvidlemap  12829  dvcnp2cntop  12832  dvaddxxbr  12834  dvmulxxbr  12835  dviaddf  12838  dvexp  12844  dvmptaddx  12850  dvmptmulx  12851  dvef  12856  sincn  12858  coscn  12859  nninfsellemeqinf  13212  nninffeq  13216  exmidsbthrlem  13217  cvgcmp2nlemabs  13227