Theorem eqidd 2235

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 2234	. 2 |- A = A
2	1	a1i 9	1 |- ( ph -> A = A )

Syntax hints:   -> wi 4   = wceq 1398

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 1498  ax-ext 2216

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

This theorem is referenced by:  cbvraldva  2789  cbvrexdva  2790  rspcedeq1vd  2933  rspcedeq2vd  2934  nelrdva  3027  opeq2  3889  mpteq1  4199  tfisi  4714  feq23d  5509  f10d  5655  fvmptdv2  5772  elrnrexdm  5821  fmptco  5848  cofmpt  5851  ftpg  5873  fliftfun  5975  fliftval  5979  cbvmpo  6140  fconstmpo  6156  eqfnov2  6169  ovmpod  6189  ovmpodv2  6195  fvmpopr2d  6198  elovmporab  6262  elovmporab1w  6263  ofvalg  6285  ofrval  6286  off  6288  ofres  6290  suppssof1  6293  ofco  6294  caofref  6300  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  caofrss  6307  caoftrn  6308  uchoice  6344  suppofss1dcl  6477  suppofss2dcl  6478  rdgivallem  6625  iserd  6806  ixpsnf1o  6984  modom  7074  1domsn  7081  mapxpen  7114  infnninf  7428  ctssexmid  7454  nninfdcinf  7475  nninfwlporlemd  7476  nninfwlporlem  7477  nninfwlpoimlemginf  7480  nninfinfwlpo  7484  ofnegsub  9253  infrenegsupex  9944  fz0to4untppr  10480  fzo0to3tp  10586  modqsubmod  10768  0tonninf  10826  iseqovex  10844  seqvalcd  10847  seq3f1olemqsumkj  10897  seq3id  10911  seq3id2  10912  ccatws1ls  11355  pfxsuffeqwrdeq  11415  wrdind  11439  wrd2ind  11440  ccats1pfxeqbi  11459  s3eq2  11494  resqrexlemp1rp  11716  resqrexlemfp1  11719  resqrex  11736  infxrnegsupex  11973  climcl  11992  clim2  11993  climuni  12003  climeq  12009  2clim  12011  climshftlemg  12012  climabs0  12017  climcn1  12018  climcn2  12019  climge0  12035  climsqz  12045  climsqz2  12046  climcau  12057  climrecvg1n  12058  climcaucn  12061  serf0  12062  fzf1o  12086  isumz  12100  fisumss  12103  fsumsplitsn  12121  fsumsplitsnun  12130  isumclim3  12134  isummulc2  12137  fsum2dlemstep  12145  fsumconst  12165  fsumabs  12176  fsumparts  12181  iserabs  12186  fsumiun  12188  isumshft  12201  cvgratnnlemseq  12237  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  prod1dc  12297  fprodssdc  12301  fprodunsn  12315  fprodcl2lem  12316  fprodconst  12331  fprod2dlemstep  12333  fprodsplitsn  12344  eftlcl  12399  reeftlcl  12400  eftlub  12401  efsep  12402  effsumlt  12403  eirraplem  12488  2tp1odd  12595  bezoutlemstep  12718  nninfctlemfo  12761  alginv  12769  algfx  12774  cncongr1  12825  qnumdencoprm  12915  qeqnumdivden  12916  ballotfilemgun  13212  ballotfilemfg  13213  ballotfilemfrc  13214  ctiunctal  13276  unct  13277  nninfdclemcl  13283  nninfdclemf  13284  nninfdclemp1  13285  nninfdc  13288  ressbasid  13367  ressressg  13372  imasex  13569  imasbas  13571  imasplusg  13572  imasmulr  13573  qusin  13590  igsumvalx  13652  gsumfzval  13654  gsumpropd  13655  gsumpropd2  13656  gsum0g  13659  gsumval2  13660  issgrp  13666  sgrp1  13674  issgrpd  13675  ismndd  13698  mndprop  13702  ress0g  13704  imasmnd2  13707  insubm  13740  resmhm  13742  resmhm2  13743  resmhm2b  13744  gsumfzz  13750  grpprop  13773  grpsubfvalg  13800  grpressid  13816  grpsubpropdg  13859  imasgrp2  13863  imasgrp  13864  imasgrpf1  13865  mulgfvalg  13874  mulgnngsum  13880  mulgpropdg  13917  submmulg  13919  subginv  13934  subgcl  13937  subgsub  13939  releqgg  13973  eqgex  13974  eqgfval  13975  qusgrp  13985  resghm  14013  ablprop  14050  subcmnd  14086  ablressid  14088  gsumfzmptfidmadd  14092  gsumfzconst  14094  gsumfzconstf  14095  gsumfzmhm2  14097  gsumsplit0  14099  gfsumval  14102  gsumshift  14105  gsumgfsum  14106  gfsumsn  14107  gfsumz  14109  prdsex  14114  prdsbaslemss  14116  prdssca  14117  prdsbas  14118  prdsplusg  14119  prdsmulr  14120  prdssgrpd  14133  prdsmndd  14136  prdsgrpd  14139  isrng  14173  isrngd  14192  rngressid  14193  imasrng  14195  issrg  14208  srgidmlem  14221  isring  14243  ringass  14259  ringidmlem  14265  ringabl  14275  ringprop  14283  isringd  14284  ring1  14302  ringressid  14306  imasring  14307  opprrng  14320  opprring  14322  opprringbg  14323  opprsubgg  14328  mulgass3  14329  dvdsrcld  14342  dvdsrex  14343  dvdsrcl2  14344  dvdsrid  14345  dvdsrtr  14346  dvdsrneg  14348  dvdsr01  14349  1unit  14352  unitcld  14353  opprunitd  14355  crngunit  14356  unitmulcl  14358  unitgrpbasd  14360  unitgrp  14361  unitabl  14362  unitgrpid  14363  unitsubm  14364  unitlinv  14371  unitrinv  14372  unitnegcl  14375  dvrfvald  14378  dvrvald  14379  dvrcl  14380  unitdvcl  14381  dvrid  14382  dvr1  14383  dvrdir  14388  rdivmuldivd  14389  dvdsrpropdg  14392  unitpropdg  14393  invrpropdg  14394  rhmf1o  14413  rhmdvdsr  14420  elrhmunit  14422  rhmunitinv  14423  opprlring  14442  issubrng2  14456  subrngpropd  14462  subrgcrng  14471  subrgdvds  14481  subrguss  14482  subrginv  14483  subrgdv  14484  subrgunit  14485  subrgugrp  14486  issubrg2  14487  subrgpropd  14499  aprunit  14530  aprirr  14533  aprsym  14534  aprcotr  14535  aprap  14536  aprnzr  14537  aprlring  14538  aprprop  14539  opprdrng  14558  islmodd  14567  lmodabl  14608  lss1  14636  lsssn0  14644  islss3  14653  lss1d  14657  lssintclm  14658  lsslsp  14703  sralmod  14724  sralmod0g  14725  rlmfn  14727  rlmvalg  14728  rlm0g  14731  rlmvnegg  14739  lidlssbas  14751  islidlm  14753  rnglidlmsgrp  14771  rnglidlrng  14772  qus2idrng  14799  crngridl  14804  quscrng  14807  cnfldui  14863  dvdsrzring  14877  zrhpropd  14900  znzrh  14917  znbas  14918  zncrng  14919  znzrhfo  14922  znf1o  14925  znunit  14933  psrval  14940  psrbaglesuppg  14947  psrbagcon  14952  psrbagconf1o  14954  psrbasg  14955  psrplusgg  14959  mplsubgfilemcl  14980  mplplusgg  14984  epttop  15081  lmss  15237  txlm  15270  lmcn2  15271  cnmpt2c  15281  txswaphmeolem  15311  blfvalps  15376  bdxmet  15492  mpomulcn  15557  fsumcncntop  15558  cncfmptc  15587  cncfmpt1f  15589  cdivcncfap  15595  negfcncf  15597  divcncfap  15605  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dviaddf  15696  dvexp  15702  dvmptaddx  15710  dvmptmulx  15711  dvmptfsum  15716  dvef  15718  elply2  15726  elplyr  15731  plyaddlem1  15738  plycolemc  15749  sincn  15760  coscn  15761  lgsdir2lem5  16031  gausslemma2dlem1  16060  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgsquad2lem2  16081  2lgslem1b  16088  2lgslem3b1  16097  2lgslem3c1  16098  2lgsoddprmlem4  16111  2sqlem8  16122  usgredg4  16336  ushgredgedg  16347  ushgredgedgloop  16349  usgrstrrepeen  16352  uspgr1edc  16361  wlk1walkdom  16480  uspgr2wlkeq  16486  uspgr2wlkeqi  16488  clwwlknonmpo  16549  iseupth  16568  eupth2lem2dc  16580  konigsberglem2  16610  konigsberglem3  16611  nninfsellemeqinf  16920  nninffeq  16924  nnnninfex  16926  exmidsbthrlem  16928  cvgcmp2nlemabs  16942