Theorem eqidd 2194

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	|- ( ph -> A = A )

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2193	. 2 |- A = A
2	1	a1i 9	1 |- ( ph -> A = A )

Syntax hints:   -> wi 4   = wceq 1364

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 1460  ax-ext 2175

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

This theorem is referenced by:  cbvraldva  2735  cbvrexdva  2736  rspcedeq1vd  2873  rspcedeq2vd  2874  nelrdva  2967  opeq2  3805  mpteq1  4113  tfisi  4619  feq23d  5399  fvmptdv2  5647  elrnrexdm  5697  fmptco  5724  cofmpt  5727  ftpg  5742  fliftfun  5839  fliftval  5843  cbvmpo  5997  fconstmpo  6013  eqfnov2  6026  ovmpod  6046  ovmpodv2  6052  elovmporab  6118  elovmporab1w  6119  ofvalg  6140  ofrval  6141  off  6143  ofres  6145  suppssof1  6148  ofco  6149  caofref  6154  caofrss  6157  caoftrn  6158  uchoice  6190  rdgivallem  6434  iserd  6613  ixpsnf1o  6790  1domsn  6873  mapxpen  6904  infnninf  7183  ctssexmid  7209  nninfdcinf  7230  nninfwlporlemd  7231  nninfwlporlem  7232  nninfwlpoimlemginf  7235  ofnegsub  8981  infrenegsupex  9659  fz0to4untppr  10190  fzo0to3tp  10286  modqsubmod  10453  0tonninf  10511  iseqovex  10529  seqvalcd  10532  seq3f1olemqsumkj  10582  seq3id  10596  seq3id2  10597  resqrexlemp1rp  11150  resqrexlemfp1  11153  resqrex  11170  infxrnegsupex  11406  climcl  11425  clim2  11426  climuni  11436  climeq  11442  2clim  11444  climshftlemg  11445  climabs0  11450  climcn1  11451  climcn2  11452  climge0  11468  climsqz  11478  climsqz2  11479  climcau  11490  climrecvg1n  11491  climcaucn  11494  serf0  11495  isumz  11532  fisumss  11535  fsumsplitsn  11553  fsumsplitsnun  11562  isumclim3  11566  isummulc2  11569  fsum2dlemstep  11577  fsumconst  11597  fsumabs  11608  fsumparts  11613  iserabs  11618  fsumiun  11620  isumshft  11633  cvgratnnlemseq  11669  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  prod1dc  11729  fprodssdc  11733  fprodunsn  11747  fprodcl2lem  11748  fprodconst  11763  fprod2dlemstep  11765  fprodsplitsn  11776  eftlcl  11831  reeftlcl  11832  eftlub  11833  efsep  11834  effsumlt  11835  eirraplem  11920  2tp1odd  12025  bezoutlemstep  12134  nninfctlemfo  12177  alginv  12185  algfx  12190  cncongr1  12241  qnumdencoprm  12331  qeqnumdivden  12332  ctiunctal  12598  unct  12599  nninfdclemcl  12605  nninfdclemf  12606  nninfdclemp1  12607  nninfdc  12610  ressbasid  12688  ressressg  12693  prdsex  12880  imasex  12888  imasbas  12890  imasplusg  12891  imasmulr  12892  qusin  12909  igsumvalx  12972  gsumfzval  12974  gsumpropd  12975  gsumpropd2  12976  gsum0g  12979  gsumval2  12980  issgrp  12986  sgrp1  12994  issgrpd  12995  ismndd  13018  mndprop  13022  ress0g  13024  insubm  13057  resmhm  13059  resmhm2  13060  resmhm2b  13061  gsumfzz  13067  grpprop  13090  grpsubfvalg  13117  grpressid  13133  grpsubpropdg  13176  imasgrp2  13180  imasgrp  13181  imasgrpf1  13182  mulgfvalg  13191  mulgnngsum  13197  mulgpropdg  13234  submmulg  13236  subginv  13251  subgcl  13254  subgsub  13256  releqgg  13290  eqgex  13291  eqgfval  13292  qusgrp  13302  resghm  13330  ablprop  13367  subcmnd  13403  ablressid  13405  gsumfzmptfidmadd  13409  gsumfzconst  13411  gsumfzconstf  13412  gsumfzmhm2  13414  isrng  13430  isrngd  13449  rngressid  13450  imasrng  13452  issrg  13461  srgidmlem  13474  isring  13496  ringass  13512  ringidmlem  13518  ringabl  13528  ringprop  13536  isringd  13537  ring1  13555  ringressid  13559  imasring  13560  opprrng  13573  opprring  13575  opprringbg  13576  opprsubgg  13580  mulgass3  13581  dvdsrcld  13593  dvdsrex  13594  dvdsrcl2  13595  dvdsrid  13596  dvdsrtr  13597  dvdsrneg  13599  dvdsr01  13600  1unit  13603  unitcld  13604  opprunitd  13606  crngunit  13607  unitmulcl  13609  unitgrpbasd  13611  unitgrp  13612  unitabl  13613  unitgrpid  13614  unitsubm  13615  unitlinv  13622  unitrinv  13623  unitnegcl  13626  dvrfvald  13629  dvrvald  13630  dvrcl  13631  unitdvcl  13632  dvrid  13633  dvr1  13634  dvrdir  13639  rdivmuldivd  13640  dvdsrpropdg  13643  unitpropdg  13644  invrpropdg  13645  rhmf1o  13664  rhmdvdsr  13671  elrhmunit  13673  rhmunitinv  13674  issubrng2  13706  subrngpropd  13712  subrgcrng  13721  subrgdvds  13731  subrguss  13732  subrginv  13733  subrgdv  13734  subrgunit  13735  subrgugrp  13736  issubrg2  13737  subrgpropd  13749  aprirr  13779  aprsym  13780  aprcotr  13781  aprap  13782  islmodd  13789  lmodabl  13830  lss1  13858  lsssn0  13866  islss3  13875  lss1d  13879  lssintclm  13880  lsslsp  13925  sralmod  13946  sralmod0g  13947  rlmfn  13949  rlmvalg  13950  rlm0g  13953  rlmvnegg  13961  lidlssbas  13973  islidlm  13975  rnglidlmsgrp  13993  rnglidlrng  13994  qus2idrng  14021  crngridl  14026  quscrng  14029  cnfldui  14077  dvdsrzring  14091  zrhpropd  14114  znzrh  14131  znbas  14132  zncrng  14133  znzrhfo  14136  znf1o  14139  znunit  14147  psrval  14152  psrbaglesuppg  14158  psrbasg  14159  psrplusgg  14162  epttop  14258  lmss  14414  txlm  14447  lmcn2  14448  cnmpt2c  14458  txswaphmeolem  14488  blfvalps  14553  bdxmet  14669  fsumcncntop  14724  cncfmptc  14750  cncfmpt1f  14752  cdivcncfap  14758  negfcncf  14760  divcncfap  14768  dvidlemap  14845  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  dviaddf  14854  dvexp  14860  dvmptaddx  14866  dvmptmulx  14867  dvef  14873  elply2  14881  elplyr  14886  plyaddlem1  14893  sincn  14904  coscn  14905  lgsdir2lem5  15148  gausslemma2dlem1  15177  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  2lgsoddprmlem4  15200  2sqlem8  15210  nninfsellemeqinf  15506  nninffeq  15510  exmidsbthrlem  15512  cvgcmp2nlemabs  15522