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  2916  rspcedeq2vd  2917  nelrdva  3010  opeq2  3857  mpteq1  4167  tfisi  4678  feq23d  5468  f10d  5606  fvmptdv2  5723  elrnrexdm  5773  fmptco  5800  cofmpt  5803  ftpg  5822  fliftfun  5919  fliftval  5923  cbvmpo  6082  fconstmpo  6098  eqfnov2  6111  ovmpod  6131  ovmpodv2  6137  fvmpopr2d  6140  elovmporab  6204  elovmporab1w  6205  ofvalg  6226  ofrval  6227  off  6229  ofres  6231  suppssof1  6234  ofco  6235  caofref  6241  caofid0l  6243  caofid0r  6244  caofid1  6245  caofid2  6246  caofrss  6248  caoftrn  6249  uchoice  6281  rdgivallem  6525  iserd  6704  ixpsnf1o  6881  1domsn  6974  mapxpen  7005  infnninf  7287  ctssexmid  7313  nninfdcinf  7334  nninfwlporlemd  7335  nninfwlporlem  7336  nninfwlpoimlemginf  7339  nninfinfwlpo  7343  ofnegsub  9105  infrenegsupex  9785  fz0to4untppr  10316  fzo0to3tp  10420  modqsubmod  10599  0tonninf  10657  iseqovex  10675  seqvalcd  10678  seq3f1olemqsumkj  10728  seq3id  10742  seq3id2  10743  ccatws1ls  11168  pfxsuffeqwrdeq  11225  wrdind  11249  wrd2ind  11250  ccats1pfxeqbi  11269  s3eq2  11304  resqrexlemp1rp  11512  resqrexlemfp1  11515  resqrex  11532  infxrnegsupex  11769  climcl  11788  clim2  11789  climuni  11799  climeq  11805  2clim  11807  climshftlemg  11808  climabs0  11813  climcn1  11814  climcn2  11815  climge0  11831  climsqz  11841  climsqz2  11842  climcau  11853  climrecvg1n  11854  climcaucn  11857  serf0  11858  isumz  11895  fisumss  11898  fsumsplitsn  11916  fsumsplitsnun  11925  isumclim3  11929  isummulc2  11932  fsum2dlemstep  11940  fsumconst  11960  fsumabs  11971  fsumparts  11976  iserabs  11981  fsumiun  11983  isumshft  11996  cvgratnnlemseq  12032  mertenslemub  12040  mertenslemi1  12041  mertenslem2  12042  prod1dc  12092  fprodssdc  12096  fprodunsn  12110  fprodcl2lem  12111  fprodconst  12126  fprod2dlemstep  12128  fprodsplitsn  12139  eftlcl  12194  reeftlcl  12195  eftlub  12196  efsep  12197  effsumlt  12198  eirraplem  12283  2tp1odd  12390  bezoutlemstep  12513  nninfctlemfo  12556  alginv  12564  algfx  12569  cncongr1  12620  qnumdencoprm  12710  qeqnumdivden  12711  ctiunctal  13007  unct  13008  nninfdclemcl  13014  nninfdclemf  13015  nninfdclemp1  13016  nninfdc  13019  ressbasid  13098  ressressg  13103  prdsex  13297  prdsbaslemss  13302  prdssca  13303  prdsbas  13304  prdsplusg  13305  prdsmulr  13306  imasex  13333  imasbas  13335  imasplusg  13336  imasmulr  13337  qusin  13354  igsumvalx  13417  gsumfzval  13419  gsumpropd  13420  gsumpropd2  13421  gsum0g  13424  gsumval2  13425  issgrp  13431  sgrp1  13439  issgrpd  13440  prdssgrpd  13443  ismndd  13465  mndprop  13469  ress0g  13471  prdsmndd  13476  imasmnd2  13480  insubm  13513  resmhm  13515  resmhm2  13516  resmhm2b  13517  gsumfzz  13523  grpprop  13546  grpsubfvalg  13573  grpressid  13589  grpsubpropdg  13632  prdsgrpd  13637  imasgrp2  13642  imasgrp  13643  imasgrpf1  13644  mulgfvalg  13653  mulgnngsum  13659  mulgpropdg  13696  submmulg  13698  subginv  13713  subgcl  13716  subgsub  13718  releqgg  13752  eqgex  13753  eqgfval  13754  qusgrp  13764  resghm  13792  ablprop  13829  subcmnd  13865  ablressid  13867  gsumfzmptfidmadd  13871  gsumfzconst  13873  gsumfzconstf  13874  gsumfzmhm2  13876  isrng  13892  isrngd  13911  rngressid  13912  imasrng  13914  issrg  13923  srgidmlem  13936  isring  13958  ringass  13974  ringidmlem  13980  ringabl  13990  ringprop  13998  isringd  13999  ring1  14017  ringressid  14021  imasring  14022  opprrng  14035  opprring  14037  opprringbg  14038  opprsubgg  14042  mulgass3  14043  dvdsrcld  14055  dvdsrex  14056  dvdsrcl2  14057  dvdsrid  14058  dvdsrtr  14059  dvdsrneg  14061  dvdsr01  14062  1unit  14065  unitcld  14066  opprunitd  14068  crngunit  14069  unitmulcl  14071  unitgrpbasd  14073  unitgrp  14074  unitabl  14075  unitgrpid  14076  unitsubm  14077  unitlinv  14084  unitrinv  14085  unitnegcl  14088  dvrfvald  14091  dvrvald  14092  dvrcl  14093  unitdvcl  14094  dvrid  14095  dvr1  14096  dvrdir  14101  rdivmuldivd  14102  dvdsrpropdg  14105  unitpropdg  14106  invrpropdg  14107  rhmf1o  14126  rhmdvdsr  14133  elrhmunit  14135  rhmunitinv  14136  issubrng2  14168  subrngpropd  14174  subrgcrng  14183  subrgdvds  14193  subrguss  14194  subrginv  14195  subrgdv  14196  subrgunit  14197  subrgugrp  14198  issubrg2  14199  subrgpropd  14211  aprirr  14241  aprsym  14242  aprcotr  14243  aprap  14244  islmodd  14251  lmodabl  14292  lss1  14320  lsssn0  14328  islss3  14337  lss1d  14341  lssintclm  14342  lsslsp  14387  sralmod  14408  sralmod0g  14409  rlmfn  14411  rlmvalg  14412  rlm0g  14415  rlmvnegg  14423  lidlssbas  14435  islidlm  14437  rnglidlmsgrp  14455  rnglidlrng  14456  qus2idrng  14483  crngridl  14488  quscrng  14491  cnfldui  14547  dvdsrzring  14561  zrhpropd  14584  znzrh  14601  znbas  14602  zncrng  14603  znzrhfo  14606  znf1o  14609  znunit  14617  psrval  14624  psrbaglesuppg  14630  psrbasg  14632  psrplusgg  14636  mplsubgfilemcl  14657  mplplusgg  14661  epttop  14758  lmss  14914  txlm  14947  lmcn2  14948  cnmpt2c  14958  txswaphmeolem  14988  blfvalps  15053  bdxmet  15169  mpomulcn  15234  fsumcncntop  15235  cncfmptc  15264  cncfmpt1f  15266  cdivcncfap  15272  negfcncf  15274  divcncfap  15282  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dviaddf  15373  dvexp  15379  dvmptaddx  15387  dvmptmulx  15388  dvmptfsum  15393  dvef  15395  elply2  15403  elplyr  15408  plyaddlem1  15415  plycolemc  15426  sincn  15437  coscn  15438  lgsdir2lem5  15705  gausslemma2dlem1  15734  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgsquad2lem2  15755  2lgslem1b  15762  2lgslem3b1  15771  2lgslem3c1  15772  2lgsoddprmlem4  15785  2sqlem8  15796  usgredg4  16007  ushgredgedg  16018  ushgredgedgloop  16020  usgrstrrepeen  16023  nninfsellemeqinf  16341  nninffeq  16345  nnnninfex  16347  exmidsbthrlem  16349  cvgcmp2nlemabs  16359