Theorem eqidd 2230

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

Syntax hints:   -> wi 4   = wceq 1395

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 1495  ax-ext 2211

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

This theorem is referenced by:  cbvraldva  2774  cbvrexdva  2775  rspcedeq1vd  2917  rspcedeq2vd  2918  nelrdva  3011  opeq2  3861  mpteq1  4171  tfisi  4683  feq23d  5475  f10d  5615  fvmptdv2  5732  elrnrexdm  5782  fmptco  5809  cofmpt  5812  ftpg  5833  fliftfun  5932  fliftval  5936  cbvmpo  6095  fconstmpo  6111  eqfnov2  6124  ovmpod  6144  ovmpodv2  6150  fvmpopr2d  6153  elovmporab  6217  elovmporab1w  6218  ofvalg  6240  ofrval  6241  off  6243  ofres  6245  suppssof1  6248  ofco  6249  caofref  6255  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  caofrss  6262  caoftrn  6263  uchoice  6295  rdgivallem  6542  iserd  6723  ixpsnf1o  6900  modom  6989  1domsn  6996  mapxpen  7029  infnninf  7314  ctssexmid  7340  nninfdcinf  7361  nninfwlporlemd  7362  nninfwlporlem  7363  nninfwlpoimlemginf  7366  nninfinfwlpo  7370  ofnegsub  9132  infrenegsupex  9818  fz0to4untppr  10349  fzo0to3tp  10454  modqsubmod  10634  0tonninf  10692  iseqovex  10710  seqvalcd  10713  seq3f1olemqsumkj  10763  seq3id  10777  seq3id2  10778  ccatws1ls  11209  pfxsuffeqwrdeq  11269  wrdind  11293  wrd2ind  11294  ccats1pfxeqbi  11313  s3eq2  11348  resqrexlemp1rp  11557  resqrexlemfp1  11560  resqrex  11577  infxrnegsupex  11814  climcl  11833  clim2  11834  climuni  11844  climeq  11850  2clim  11852  climshftlemg  11853  climabs0  11858  climcn1  11859  climcn2  11860  climge0  11876  climsqz  11886  climsqz2  11887  climcau  11898  climrecvg1n  11899  climcaucn  11902  serf0  11903  isumz  11940  fisumss  11943  fsumsplitsn  11961  fsumsplitsnun  11970  isumclim3  11974  isummulc2  11977  fsum2dlemstep  11985  fsumconst  12005  fsumabs  12016  fsumparts  12021  iserabs  12026  fsumiun  12028  isumshft  12041  cvgratnnlemseq  12077  mertenslemub  12085  mertenslemi1  12086  mertenslem2  12087  prod1dc  12137  fprodssdc  12141  fprodunsn  12155  fprodcl2lem  12156  fprodconst  12171  fprod2dlemstep  12173  fprodsplitsn  12184  eftlcl  12239  reeftlcl  12240  eftlub  12241  efsep  12242  effsumlt  12243  eirraplem  12328  2tp1odd  12435  bezoutlemstep  12558  nninfctlemfo  12601  alginv  12609  algfx  12614  cncongr1  12665  qnumdencoprm  12755  qeqnumdivden  12756  ctiunctal  13052  unct  13053  nninfdclemcl  13059  nninfdclemf  13060  nninfdclemp1  13061  nninfdc  13064  ressbasid  13143  ressressg  13148  prdsex  13342  prdsbaslemss  13347  prdssca  13348  prdsbas  13349  prdsplusg  13350  prdsmulr  13351  imasex  13378  imasbas  13380  imasplusg  13381  imasmulr  13382  qusin  13399  igsumvalx  13462  gsumfzval  13464  gsumpropd  13465  gsumpropd2  13466  gsum0g  13469  gsumval2  13470  issgrp  13476  sgrp1  13484  issgrpd  13485  prdssgrpd  13488  ismndd  13510  mndprop  13514  ress0g  13516  prdsmndd  13521  imasmnd2  13525  insubm  13558  resmhm  13560  resmhm2  13561  resmhm2b  13562  gsumfzz  13568  grpprop  13591  grpsubfvalg  13618  grpressid  13634  grpsubpropdg  13677  prdsgrpd  13682  imasgrp2  13687  imasgrp  13688  imasgrpf1  13689  mulgfvalg  13698  mulgnngsum  13704  mulgpropdg  13741  submmulg  13743  subginv  13758  subgcl  13761  subgsub  13763  releqgg  13797  eqgex  13798  eqgfval  13799  qusgrp  13809  resghm  13837  ablprop  13874  subcmnd  13910  ablressid  13912  gsumfzmptfidmadd  13916  gsumfzconst  13918  gsumfzconstf  13919  gsumfzmhm2  13921  isrng  13937  isrngd  13956  rngressid  13957  imasrng  13959  issrg  13968  srgidmlem  13981  isring  14003  ringass  14019  ringidmlem  14025  ringabl  14035  ringprop  14043  isringd  14044  ring1  14062  ringressid  14066  imasring  14067  opprrng  14080  opprring  14082  opprringbg  14083  opprsubgg  14087  mulgass3  14088  dvdsrcld  14101  dvdsrex  14102  dvdsrcl2  14103  dvdsrid  14104  dvdsrtr  14105  dvdsrneg  14107  dvdsr01  14108  1unit  14111  unitcld  14112  opprunitd  14114  crngunit  14115  unitmulcl  14117  unitgrpbasd  14119  unitgrp  14120  unitabl  14121  unitgrpid  14122  unitsubm  14123  unitlinv  14130  unitrinv  14131  unitnegcl  14134  dvrfvald  14137  dvrvald  14138  dvrcl  14139  unitdvcl  14140  dvrid  14141  dvr1  14142  dvrdir  14147  rdivmuldivd  14148  dvdsrpropdg  14151  unitpropdg  14152  invrpropdg  14153  rhmf1o  14172  rhmdvdsr  14179  elrhmunit  14181  rhmunitinv  14182  issubrng2  14214  subrngpropd  14220  subrgcrng  14229  subrgdvds  14239  subrguss  14240  subrginv  14241  subrgdv  14242  subrgunit  14243  subrgugrp  14244  issubrg2  14245  subrgpropd  14257  aprirr  14287  aprsym  14288  aprcotr  14289  aprap  14290  islmodd  14297  lmodabl  14338  lss1  14366  lsssn0  14374  islss3  14383  lss1d  14387  lssintclm  14388  lsslsp  14433  sralmod  14454  sralmod0g  14455  rlmfn  14457  rlmvalg  14458  rlm0g  14461  rlmvnegg  14469  lidlssbas  14481  islidlm  14483  rnglidlmsgrp  14501  rnglidlrng  14502  qus2idrng  14529  crngridl  14534  quscrng  14537  cnfldui  14593  dvdsrzring  14607  zrhpropd  14630  znzrh  14647  znbas  14648  zncrng  14649  znzrhfo  14652  znf1o  14655  znunit  14663  psrval  14670  psrbaglesuppg  14676  psrbasg  14678  psrplusgg  14682  mplsubgfilemcl  14703  mplplusgg  14707  epttop  14804  lmss  14960  txlm  14993  lmcn2  14994  cnmpt2c  15004  txswaphmeolem  15034  blfvalps  15099  bdxmet  15215  mpomulcn  15280  fsumcncntop  15281  cncfmptc  15310  cncfmpt1f  15312  cdivcncfap  15318  negfcncf  15320  divcncfap  15328  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dviaddf  15419  dvexp  15425  dvmptaddx  15433  dvmptmulx  15434  dvmptfsum  15439  dvef  15441  elply2  15449  elplyr  15454  plyaddlem1  15461  plycolemc  15472  sincn  15483  coscn  15484  lgsdir2lem5  15751  gausslemma2dlem1  15780  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgsquad2lem2  15801  2lgslem1b  15808  2lgslem3b1  15817  2lgslem3c1  15818  2lgsoddprmlem4  15831  2sqlem8  15842  usgredg4  16054  ushgredgedg  16065  ushgredgedgloop  16067  usgrstrrepeen  16070  uspgr1edc  16079  wlk1walkdom  16156  uspgr2wlkeq  16162  uspgr2wlkeqi  16164  clwwlknonmpo  16223  iseupth  16242  nninfsellemeqinf  16554  nninffeq  16558  nnnninfex  16560  exmidsbthrlem  16562  cvgcmp2nlemabs  16572