Theorem eqidd 2232

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 2231	. 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 2213

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

This theorem is referenced by:  cbvraldva  2777  cbvrexdva  2778  rspcedeq1vd  2920  rspcedeq2vd  2921  nelrdva  3014  opeq2  3868  mpteq1  4178  tfisi  4691  feq23d  5485  f10d  5628  fvmptdv2  5745  elrnrexdm  5794  fmptco  5821  cofmpt  5824  ftpg  5846  fliftfun  5947  fliftval  5951  cbvmpo  6110  fconstmpo  6126  eqfnov2  6139  ovmpod  6159  ovmpodv2  6165  fvmpopr2d  6168  elovmporab  6232  elovmporab1w  6233  ofvalg  6254  ofrval  6255  off  6257  ofres  6259  suppssof1  6262  ofco  6263  caofref  6269  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  caofrss  6276  caoftrn  6277  uchoice  6309  suppofss1dcl  6442  suppofss2dcl  6443  rdgivallem  6590  iserd  6771  ixpsnf1o  6948  modom  7037  1domsn  7044  mapxpen  7077  infnninf  7366  ctssexmid  7392  nninfdcinf  7413  nninfwlporlemd  7414  nninfwlporlem  7415  nninfwlpoimlemginf  7418  nninfinfwlpo  7422  ofnegsub  9184  infrenegsupex  9872  fz0to4untppr  10404  fzo0to3tp  10510  modqsubmod  10690  0tonninf  10748  iseqovex  10766  seqvalcd  10769  seq3f1olemqsumkj  10819  seq3id  10833  seq3id2  10834  ccatws1ls  11268  pfxsuffeqwrdeq  11328  wrdind  11352  wrd2ind  11353  ccats1pfxeqbi  11372  s3eq2  11407  resqrexlemp1rp  11629  resqrexlemfp1  11632  resqrex  11649  infxrnegsupex  11886  climcl  11905  clim2  11906  climuni  11916  climeq  11922  2clim  11924  climshftlemg  11925  climabs0  11930  climcn1  11931  climcn2  11932  climge0  11948  climsqz  11958  climsqz2  11959  climcau  11970  climrecvg1n  11971  climcaucn  11974  serf0  11975  fzf1o  11999  isumz  12013  fisumss  12016  fsumsplitsn  12034  fsumsplitsnun  12043  isumclim3  12047  isummulc2  12050  fsum2dlemstep  12058  fsumconst  12078  fsumabs  12089  fsumparts  12094  iserabs  12099  fsumiun  12101  isumshft  12114  cvgratnnlemseq  12150  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  prod1dc  12210  fprodssdc  12214  fprodunsn  12228  fprodcl2lem  12229  fprodconst  12244  fprod2dlemstep  12246  fprodsplitsn  12257  eftlcl  12312  reeftlcl  12313  eftlub  12314  efsep  12315  effsumlt  12316  eirraplem  12401  2tp1odd  12508  bezoutlemstep  12631  nninfctlemfo  12674  alginv  12682  algfx  12687  cncongr1  12738  qnumdencoprm  12828  qeqnumdivden  12829  ctiunctal  13125  unct  13126  nninfdclemcl  13132  nninfdclemf  13133  nninfdclemp1  13134  nninfdc  13137  ressbasid  13216  ressressg  13221  prdsex  13415  prdsbaslemss  13420  prdssca  13421  prdsbas  13422  prdsplusg  13423  prdsmulr  13424  imasex  13451  imasbas  13453  imasplusg  13454  imasmulr  13455  qusin  13472  igsumvalx  13535  gsumfzval  13537  gsumpropd  13538  gsumpropd2  13539  gsum0g  13542  gsumval2  13543  issgrp  13549  sgrp1  13557  issgrpd  13558  prdssgrpd  13561  ismndd  13583  mndprop  13587  ress0g  13589  prdsmndd  13594  imasmnd2  13598  insubm  13631  resmhm  13633  resmhm2  13634  resmhm2b  13635  gsumfzz  13641  grpprop  13664  grpsubfvalg  13691  grpressid  13707  grpsubpropdg  13750  prdsgrpd  13755  imasgrp2  13760  imasgrp  13761  imasgrpf1  13762  mulgfvalg  13771  mulgnngsum  13777  mulgpropdg  13814  submmulg  13816  subginv  13831  subgcl  13834  subgsub  13836  releqgg  13870  eqgex  13871  eqgfval  13872  qusgrp  13882  resghm  13910  ablprop  13947  subcmnd  13983  ablressid  13985  gsumfzmptfidmadd  13989  gsumfzconst  13991  gsumfzconstf  13992  gsumfzmhm2  13994  gsumsplit0  13996  isrng  14011  isrngd  14030  rngressid  14031  imasrng  14033  issrg  14042  srgidmlem  14055  isring  14077  ringass  14093  ringidmlem  14099  ringabl  14109  ringprop  14117  isringd  14118  ring1  14136  ringressid  14140  imasring  14141  opprrng  14154  opprring  14156  opprringbg  14157  opprsubgg  14161  mulgass3  14162  dvdsrcld  14175  dvdsrex  14176  dvdsrcl2  14177  dvdsrid  14178  dvdsrtr  14179  dvdsrneg  14181  dvdsr01  14182  1unit  14185  unitcld  14186  opprunitd  14188  crngunit  14189  unitmulcl  14191  unitgrpbasd  14193  unitgrp  14194  unitabl  14195  unitgrpid  14196  unitsubm  14197  unitlinv  14204  unitrinv  14205  unitnegcl  14208  dvrfvald  14211  dvrvald  14212  dvrcl  14213  unitdvcl  14214  dvrid  14215  dvr1  14216  dvrdir  14221  rdivmuldivd  14222  dvdsrpropdg  14225  unitpropdg  14226  invrpropdg  14227  rhmf1o  14246  rhmdvdsr  14253  elrhmunit  14255  rhmunitinv  14256  issubrng2  14288  subrngpropd  14294  subrgcrng  14303  subrgdvds  14313  subrguss  14314  subrginv  14315  subrgdv  14316  subrgunit  14317  subrgugrp  14318  issubrg2  14319  subrgpropd  14331  aprirr  14362  aprsym  14363  aprcotr  14364  aprap  14365  islmodd  14372  lmodabl  14413  lss1  14441  lsssn0  14449  islss3  14458  lss1d  14462  lssintclm  14463  lsslsp  14508  sralmod  14529  sralmod0g  14530  rlmfn  14532  rlmvalg  14533  rlm0g  14536  rlmvnegg  14544  lidlssbas  14556  islidlm  14558  rnglidlmsgrp  14576  rnglidlrng  14577  qus2idrng  14604  crngridl  14609  quscrng  14612  cnfldui  14668  dvdsrzring  14682  zrhpropd  14705  znzrh  14722  znbas  14723  zncrng  14724  znzrhfo  14727  znf1o  14730  znunit  14738  psrval  14745  psrbaglesuppg  14751  psrbagcon  14755  psrbagconf1o  14757  psrbasg  14758  psrplusgg  14762  mplsubgfilemcl  14783  mplplusgg  14787  epttop  14884  lmss  15040  txlm  15073  lmcn2  15074  cnmpt2c  15084  txswaphmeolem  15114  blfvalps  15179  bdxmet  15295  mpomulcn  15360  fsumcncntop  15361  cncfmptc  15390  cncfmpt1f  15392  cdivcncfap  15398  negfcncf  15400  divcncfap  15408  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvcnp2cntop  15493  dvaddxxbr  15495  dvmulxxbr  15496  dviaddf  15499  dvexp  15505  dvmptaddx  15513  dvmptmulx  15514  dvmptfsum  15519  dvef  15521  elply2  15529  elplyr  15534  plyaddlem1  15541  plycolemc  15552  sincn  15563  coscn  15564  lgsdir2lem5  15834  gausslemma2dlem1  15863  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgsquad2lem2  15884  2lgslem1b  15891  2lgslem3b1  15900  2lgslem3c1  15901  2lgsoddprmlem4  15914  2sqlem8  15925  usgredg4  16139  ushgredgedg  16150  ushgredgedgloop  16152  usgrstrrepeen  16155  uspgr1edc  16164  wlk1walkdom  16283  uspgr2wlkeq  16289  uspgr2wlkeqi  16291  clwwlknonmpo  16352  iseupth  16371  eupth2lem2dc  16383  konigsberglem2  16413  konigsberglem3  16414  nninfsellemeqinf  16725  nninffeq  16729  nnnninfex  16731  exmidsbthrlem  16733  cvgcmp2nlemabs  16747  gfsumval  16792  gsumgfsumlem  16795  gsumgfsum  16796  gfsumsn  16797