Theorem eqidd 2178

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

Syntax hints:   → wi 4   = wceq 1353

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 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  cbvraldva  2713  cbvrexdva  2714  rspcedeq1vd  2851  rspcedeq2vd  2852  nelrdva  2945  opeq2  3780  mpteq1  4088  tfisi  4587  feq23d  5362  fvmptdv2  5606  elrnrexdm  5656  fmptco  5683  cofmpt  5686  ftpg  5701  fliftfun  5797  fliftval  5801  cbvmpo  5954  fconstmpo  5970  eqfnov2  5982  ovmpod  6002  ovmpodv2  6008  ofvalg  6092  ofrval  6093  off  6095  ofres  6097  suppssof1  6100  ofco  6101  caofref  6104  caofrss  6107  caoftrn  6108  rdgivallem  6382  iserd  6561  ixpsnf1o  6736  1domsn  6819  mapxpen  6848  infnninf  7122  ctssexmid  7148  nninfdcinf  7169  nninfwlporlemd  7170  nninfwlporlem  7171  nninfwlpoimlemginf  7174  infrenegsupex  9594  fz0to4untppr  10124  fzo0to3tp  10219  modqsubmod  10382  0tonninf  10439  iseqovex  10456  seqvalcd  10459  seq3f1olemqsumkj  10498  seq3id  10508  seq3id2  10509  resqrexlemp1rp  11015  resqrexlemfp1  11018  resqrex  11035  infxrnegsupex  11271  climcl  11290  clim2  11291  climuni  11301  climeq  11307  2clim  11309  climshftlemg  11310  climabs0  11315  climcn1  11316  climcn2  11317  climge0  11333  climsqz  11343  climsqz2  11344  climcau  11355  climrecvg1n  11356  climcaucn  11359  serf0  11360  isumz  11397  fisumss  11400  fsumsplitsn  11418  fsumsplitsnun  11427  isumclim3  11431  isummulc2  11434  fsum2dlemstep  11442  fsumconst  11462  fsumabs  11473  fsumparts  11478  iserabs  11483  fsumiun  11485  isumshft  11498  cvgratnnlemseq  11534  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  prod1dc  11594  fprodssdc  11598  fprodunsn  11612  fprodcl2lem  11613  fprodconst  11628  fprod2dlemstep  11630  fprodsplitsn  11641  eftlcl  11696  reeftlcl  11697  eftlub  11698  efsep  11699  effsumlt  11700  eirraplem  11784  2tp1odd  11889  bezoutlemstep  11998  alginv  12047  algfx  12052  cncongr1  12103  qnumdencoprm  12193  qeqnumdivden  12194  ctiunctal  12442  unct  12443  nninfdclemcl  12449  nninfdclemf  12450  nninfdclemp1  12451  nninfdc  12454  ressressg  12534  prdsex  12718  imasex  12726  imasbas  12728  imasplusg  12729  imasmulr  12730  qusin  12746  issgrp  12809  sgrp1  12816  ismndd  12838  mndprop  12842  ress0g  12844  insubm  12872  grpprop  12894  grpsubfvalg  12918  grpressid  12931  grpsubpropdg  12974  mulgfvalg  12985  mulgpropdg  13025  subginv  13041  subgcl  13044  subgsub  13046  releqgg  13080  eqgfval  13081  ablprop  13100  subcmnd  13129  issrg  13148  srgidmlem  13161  isring  13183  ringass  13199  ringidmlem  13205  ringabl  13215  ringprop  13219  isringd  13220  ring1  13236  ringressid  13238  opprring  13249  opprringbg  13250  mulgass3  13254  dvdsrcld  13266  dvdsrex  13267  dvdsrcl2  13268  dvdsrid  13269  dvdsrtr  13270  dvdsrneg  13272  dvdsr01  13273  1unit  13276  unitcld  13277  opprunitd  13279  crngunit  13280  unitmulcl  13282  unitgrpbasd  13284  unitgrp  13285  unitabl  13286  unitgrpid  13287  unitsubm  13288  unitlinv  13295  unitrinv  13296  unitnegcl  13299  dvrfvald  13302  dvrvald  13303  dvrcl  13304  unitdvcl  13305  dvrid  13306  dvr1  13307  dvrdir  13312  rdivmuldivd  13313  dvdsrpropdg  13316  unitpropdg  13317  invrpropdg  13318  subrgcrng  13346  subrgdvds  13356  subrguss  13357  subrginv  13358  subrgdv  13359  subrgunit  13360  subrgugrp  13361  issubrg2  13362  subrgpropd  13369  aprirr  13373  aprsym  13374  aprcotr  13375  aprap  13376  islmodd  13383  lmodabl  13424  dvdsrzring  13496  epttop  13593  lmss  13749  txlm  13782  lmcn2  13783  cnmpt2c  13793  txswaphmeolem  13823  blfvalps  13888  bdxmet  14004  fsumcncntop  14059  cncfmptc  14085  cncfmpt1f  14087  cdivcncfap  14090  negfcncf  14092  dvidlemap  14163  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dviaddf  14172  dvexp  14178  dvmptaddx  14184  dvmptmulx  14185  dvef  14191  sincn  14193  coscn  14194  lgsdir2lem5  14436  lgseisenlem2  14454  2lgsoddprmlem4  14463  2sqlem8  14473  nninfsellemeqinf  14768  nninffeq  14772  exmidsbthrlem  14773  cvgcmp2nlemabs  14783