Theorem eqidd 2233

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 2232	. 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 2214

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

This theorem is referenced by:  cbvraldva  2787  cbvrexdva  2788  rspcedeq1vd  2930  rspcedeq2vd  2931  nelrdva  3024  opeq2  3884  mpteq1  4194  tfisi  4709  feq23d  5504  f10d  5650  fvmptdv2  5767  elrnrexdm  5816  fmptco  5843  cofmpt  5846  ftpg  5868  fliftfun  5969  fliftval  5973  cbvmpo  6132  fconstmpo  6148  eqfnov2  6161  ovmpod  6181  ovmpodv2  6187  fvmpopr2d  6190  elovmporab  6254  elovmporab1w  6255  ofvalg  6276  ofrval  6277  off  6279  ofres  6281  suppssof1  6284  ofco  6285  caofref  6291  caofid0l  6293  caofid0r  6294  caofid1  6295  caofid2  6296  caofrss  6298  caoftrn  6299  uchoice  6331  suppofss1dcl  6464  suppofss2dcl  6465  rdgivallem  6612  iserd  6793  ixpsnf1o  6971  modom  7061  1domsn  7068  mapxpen  7101  infnninf  7415  ctssexmid  7441  nninfdcinf  7462  nninfwlporlemd  7463  nninfwlporlem  7464  nninfwlpoimlemginf  7467  nninfinfwlpo  7471  ofnegsub  9236  infrenegsupex  9926  fz0to4untppr  10458  fzo0to3tp  10564  modqsubmod  10744  0tonninf  10802  iseqovex  10820  seqvalcd  10823  seq3f1olemqsumkj  10873  seq3id  10887  seq3id2  10888  ccatws1ls  11330  pfxsuffeqwrdeq  11390  wrdind  11414  wrd2ind  11415  ccats1pfxeqbi  11434  s3eq2  11469  resqrexlemp1rp  11691  resqrexlemfp1  11694  resqrex  11711  infxrnegsupex  11948  climcl  11967  clim2  11968  climuni  11978  climeq  11984  2clim  11986  climshftlemg  11987  climabs0  11992  climcn1  11993  climcn2  11994  climge0  12010  climsqz  12020  climsqz2  12021  climcau  12032  climrecvg1n  12033  climcaucn  12036  serf0  12037  fzf1o  12061  isumz  12075  fisumss  12078  fsumsplitsn  12096  fsumsplitsnun  12105  isumclim3  12109  isummulc2  12112  fsum2dlemstep  12120  fsumconst  12140  fsumabs  12151  fsumparts  12156  iserabs  12161  fsumiun  12163  isumshft  12176  cvgratnnlemseq  12212  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  prod1dc  12272  fprodssdc  12276  fprodunsn  12290  fprodcl2lem  12291  fprodconst  12306  fprod2dlemstep  12308  fprodsplitsn  12319  eftlcl  12374  reeftlcl  12375  eftlub  12376  efsep  12377  effsumlt  12378  eirraplem  12463  2tp1odd  12570  bezoutlemstep  12693  nninfctlemfo  12736  alginv  12744  algfx  12749  cncongr1  12800  qnumdencoprm  12890  qeqnumdivden  12891  ctiunctal  13192  unct  13193  nninfdclemcl  13199  nninfdclemf  13200  nninfdclemp1  13201  nninfdc  13204  ressbasid  13283  ressressg  13288  prdsex  13482  prdsbaslemss  13487  prdssca  13488  prdsbas  13489  prdsplusg  13490  prdsmulr  13491  imasex  13518  imasbas  13520  imasplusg  13521  imasmulr  13522  qusin  13539  igsumvalx  13602  gsumfzval  13604  gsumpropd  13605  gsumpropd2  13606  gsum0g  13609  gsumval2  13610  issgrp  13616  sgrp1  13624  issgrpd  13625  prdssgrpd  13628  ismndd  13650  mndprop  13654  ress0g  13656  prdsmndd  13661  imasmnd2  13665  insubm  13698  resmhm  13700  resmhm2  13701  resmhm2b  13702  gsumfzz  13708  grpprop  13731  grpsubfvalg  13758  grpressid  13774  grpsubpropdg  13817  prdsgrpd  13822  imasgrp2  13827  imasgrp  13828  imasgrpf1  13829  mulgfvalg  13838  mulgnngsum  13844  mulgpropdg  13881  submmulg  13883  subginv  13898  subgcl  13901  subgsub  13903  releqgg  13937  eqgex  13938  eqgfval  13939  qusgrp  13949  resghm  13977  ablprop  14014  subcmnd  14050  ablressid  14052  gsumfzmptfidmadd  14056  gsumfzconst  14058  gsumfzconstf  14059  gsumfzmhm2  14061  gsumsplit0  14063  isrng  14078  isrngd  14097  rngressid  14098  imasrng  14100  issrg  14109  srgidmlem  14122  isring  14144  ringass  14160  ringidmlem  14166  ringabl  14176  ringprop  14184  isringd  14185  ring1  14203  ringressid  14207  imasring  14208  opprrng  14221  opprring  14223  opprringbg  14224  opprsubgg  14228  mulgass3  14229  dvdsrcld  14242  dvdsrex  14243  dvdsrcl2  14244  dvdsrid  14245  dvdsrtr  14246  dvdsrneg  14248  dvdsr01  14249  1unit  14252  unitcld  14253  opprunitd  14255  crngunit  14256  unitmulcl  14258  unitgrpbasd  14260  unitgrp  14261  unitabl  14262  unitgrpid  14263  unitsubm  14264  unitlinv  14271  unitrinv  14272  unitnegcl  14275  dvrfvald  14278  dvrvald  14279  dvrcl  14280  unitdvcl  14281  dvrid  14282  dvr1  14283  dvrdir  14288  rdivmuldivd  14289  dvdsrpropdg  14292  unitpropdg  14293  invrpropdg  14294  rhmf1o  14313  rhmdvdsr  14320  elrhmunit  14322  rhmunitinv  14323  issubrng2  14355  subrngpropd  14361  subrgcrng  14370  subrgdvds  14380  subrguss  14381  subrginv  14382  subrgdv  14383  subrgunit  14384  subrgugrp  14385  issubrg2  14386  subrgpropd  14398  aprirr  14429  aprsym  14430  aprcotr  14431  aprap  14432  aprnzr  14433  aprlring  14434  islmodd  14441  lmodabl  14482  lss1  14510  lsssn0  14518  islss3  14527  lss1d  14531  lssintclm  14532  lsslsp  14577  sralmod  14598  sralmod0g  14599  rlmfn  14601  rlmvalg  14602  rlm0g  14605  rlmvnegg  14613  lidlssbas  14625  islidlm  14627  rnglidlmsgrp  14645  rnglidlrng  14646  qus2idrng  14673  crngridl  14678  quscrng  14681  cnfldui  14737  dvdsrzring  14751  zrhpropd  14774  znzrh  14791  znbas  14792  zncrng  14793  znzrhfo  14796  znf1o  14799  znunit  14807  psrval  14814  psrbaglesuppg  14821  psrbagcon  14826  psrbagconf1o  14828  psrbasg  14829  psrplusgg  14833  mplsubgfilemcl  14854  mplplusgg  14858  epttop  14955  lmss  15111  txlm  15144  lmcn2  15145  cnmpt2c  15155  txswaphmeolem  15185  blfvalps  15250  bdxmet  15366  mpomulcn  15431  fsumcncntop  15432  cncfmptc  15461  cncfmpt1f  15463  cdivcncfap  15469  negfcncf  15471  divcncfap  15479  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  dviaddf  15570  dvexp  15576  dvmptaddx  15584  dvmptmulx  15585  dvmptfsum  15590  dvef  15592  elply2  15600  elplyr  15605  plyaddlem1  15612  plycolemc  15623  sincn  15634  coscn  15635  lgsdir2lem5  15905  gausslemma2dlem1  15934  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgsquad2lem2  15955  2lgslem1b  15962  2lgslem3b1  15971  2lgslem3c1  15972  2lgsoddprmlem4  15985  2sqlem8  15996  usgredg4  16210  ushgredgedg  16221  ushgredgedgloop  16223  usgrstrrepeen  16226  uspgr1edc  16235  wlk1walkdom  16354  uspgr2wlkeq  16360  uspgr2wlkeqi  16362  clwwlknonmpo  16423  iseupth  16442  eupth2lem2dc  16454  konigsberglem2  16484  konigsberglem3  16485  nninfsellemeqinf  16794  nninffeq  16798  nnnninfex  16800  exmidsbthrlem  16802  cvgcmp2nlemabs  16816  gfsumval  16862  gsumgfsumlem  16865  gsumgfsum  16866  gfsumsn  16867  gfsumz  16869