Theorem eqidd 2205

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

Syntax hints:   -> wi 4   = wceq 1372

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 1471  ax-ext 2186

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

This theorem is referenced by:  cbvraldva  2746  cbvrexdva  2747  rspcedeq1vd  2885  rspcedeq2vd  2886  nelrdva  2979  opeq2  3819  mpteq1  4127  tfisi  4634  feq23d  5420  fvmptdv2  5668  elrnrexdm  5718  fmptco  5745  cofmpt  5748  ftpg  5767  fliftfun  5864  fliftval  5868  cbvmpo  6023  fconstmpo  6039  eqfnov2  6052  ovmpod  6072  ovmpodv2  6078  fvmpopr2d  6081  elovmporab  6145  elovmporab1w  6146  ofvalg  6167  ofrval  6168  off  6170  ofres  6172  suppssof1  6175  ofco  6176  caofref  6182  caofid0l  6184  caofid0r  6185  caofid1  6186  caofid2  6187  caofrss  6189  caoftrn  6190  uchoice  6222  rdgivallem  6466  iserd  6645  ixpsnf1o  6822  1domsn  6913  mapxpen  6944  infnninf  7225  ctssexmid  7251  nninfdcinf  7272  nninfwlporlemd  7273  nninfwlporlem  7274  nninfwlpoimlemginf  7277  nninfinfwlpo  7281  ofnegsub  9034  infrenegsupex  9714  fz0to4untppr  10245  fzo0to3tp  10346  modqsubmod  10525  0tonninf  10583  iseqovex  10601  seqvalcd  10604  seq3f1olemqsumkj  10654  seq3id  10668  seq3id2  10669  ccatws1ls  11092  resqrexlemp1rp  11288  resqrexlemfp1  11291  resqrex  11308  infxrnegsupex  11545  climcl  11564  clim2  11565  climuni  11575  climeq  11581  2clim  11583  climshftlemg  11584  climabs0  11589  climcn1  11590  climcn2  11591  climge0  11607  climsqz  11617  climsqz2  11618  climcau  11629  climrecvg1n  11630  climcaucn  11633  serf0  11634  isumz  11671  fisumss  11674  fsumsplitsn  11692  fsumsplitsnun  11701  isumclim3  11705  isummulc2  11708  fsum2dlemstep  11716  fsumconst  11736  fsumabs  11747  fsumparts  11752  iserabs  11757  fsumiun  11759  isumshft  11772  cvgratnnlemseq  11808  mertenslemub  11816  mertenslemi1  11817  mertenslem2  11818  prod1dc  11868  fprodssdc  11872  fprodunsn  11886  fprodcl2lem  11887  fprodconst  11902  fprod2dlemstep  11904  fprodsplitsn  11915  eftlcl  11970  reeftlcl  11971  eftlub  11972  efsep  11973  effsumlt  11974  eirraplem  12059  2tp1odd  12166  bezoutlemstep  12289  nninfctlemfo  12332  alginv  12340  algfx  12345  cncongr1  12396  qnumdencoprm  12486  qeqnumdivden  12487  ctiunctal  12783  unct  12784  nninfdclemcl  12790  nninfdclemf  12791  nninfdclemp1  12792  nninfdc  12795  ressbasid  12873  ressressg  12878  prdsex  13072  prdsbaslemss  13077  prdssca  13078  prdsbas  13079  prdsplusg  13080  prdsmulr  13081  imasex  13108  imasbas  13110  imasplusg  13111  imasmulr  13112  qusin  13129  igsumvalx  13192  gsumfzval  13194  gsumpropd  13195  gsumpropd2  13196  gsum0g  13199  gsumval2  13200  issgrp  13206  sgrp1  13214  issgrpd  13215  prdssgrpd  13218  ismndd  13240  mndprop  13244  ress0g  13246  prdsmndd  13251  imasmnd2  13255  insubm  13288  resmhm  13290  resmhm2  13291  resmhm2b  13292  gsumfzz  13298  grpprop  13321  grpsubfvalg  13348  grpressid  13364  grpsubpropdg  13407  prdsgrpd  13412  imasgrp2  13417  imasgrp  13418  imasgrpf1  13419  mulgfvalg  13428  mulgnngsum  13434  mulgpropdg  13471  submmulg  13473  subginv  13488  subgcl  13491  subgsub  13493  releqgg  13527  eqgex  13528  eqgfval  13529  qusgrp  13539  resghm  13567  ablprop  13604  subcmnd  13640  ablressid  13642  gsumfzmptfidmadd  13646  gsumfzconst  13648  gsumfzconstf  13649  gsumfzmhm2  13651  isrng  13667  isrngd  13686  rngressid  13687  imasrng  13689  issrg  13698  srgidmlem  13711  isring  13733  ringass  13749  ringidmlem  13755  ringabl  13765  ringprop  13773  isringd  13774  ring1  13792  ringressid  13796  imasring  13797  opprrng  13810  opprring  13812  opprringbg  13813  opprsubgg  13817  mulgass3  13818  dvdsrcld  13830  dvdsrex  13831  dvdsrcl2  13832  dvdsrid  13833  dvdsrtr  13834  dvdsrneg  13836  dvdsr01  13837  1unit  13840  unitcld  13841  opprunitd  13843  crngunit  13844  unitmulcl  13846  unitgrpbasd  13848  unitgrp  13849  unitabl  13850  unitgrpid  13851  unitsubm  13852  unitlinv  13859  unitrinv  13860  unitnegcl  13863  dvrfvald  13866  dvrvald  13867  dvrcl  13868  unitdvcl  13869  dvrid  13870  dvr1  13871  dvrdir  13876  rdivmuldivd  13877  dvdsrpropdg  13880  unitpropdg  13881  invrpropdg  13882  rhmf1o  13901  rhmdvdsr  13908  elrhmunit  13910  rhmunitinv  13911  issubrng2  13943  subrngpropd  13949  subrgcrng  13958  subrgdvds  13968  subrguss  13969  subrginv  13970  subrgdv  13971  subrgunit  13972  subrgugrp  13973  issubrg2  13974  subrgpropd  13986  aprirr  14016  aprsym  14017  aprcotr  14018  aprap  14019  islmodd  14026  lmodabl  14067  lss1  14095  lsssn0  14103  islss3  14112  lss1d  14116  lssintclm  14117  lsslsp  14162  sralmod  14183  sralmod0g  14184  rlmfn  14186  rlmvalg  14187  rlm0g  14190  rlmvnegg  14198  lidlssbas  14210  islidlm  14212  rnglidlmsgrp  14230  rnglidlrng  14231  qus2idrng  14258  crngridl  14263  quscrng  14266  cnfldui  14322  dvdsrzring  14336  zrhpropd  14359  znzrh  14376  znbas  14377  zncrng  14378  znzrhfo  14381  znf1o  14384  znunit  14392  psrval  14399  psrbaglesuppg  14405  psrbasg  14407  psrplusgg  14411  mplsubgfilemcl  14432  mplplusgg  14436  epttop  14533  lmss  14689  txlm  14722  lmcn2  14723  cnmpt2c  14733  txswaphmeolem  14763  blfvalps  14828  bdxmet  14944  mpomulcn  15009  fsumcncntop  15010  cncfmptc  15039  cncfmpt1f  15041  cdivcncfap  15047  negfcncf  15049  divcncfap  15057  dvidlemap  15134  dvidrelem  15135  dvidsslem  15136  dvcnp2cntop  15142  dvaddxxbr  15144  dvmulxxbr  15145  dviaddf  15148  dvexp  15154  dvmptaddx  15162  dvmptmulx  15163  dvmptfsum  15168  dvef  15170  elply2  15178  elplyr  15183  plyaddlem1  15190  plycolemc  15201  sincn  15212  coscn  15213  lgsdir2lem5  15480  gausslemma2dlem1  15509  lgseisenlem2  15519  lgseisenlem3  15520  lgseisenlem4  15521  lgsquad2lem2  15530  2lgslem1b  15537  2lgslem3b1  15546  2lgslem3c1  15547  2lgsoddprmlem4  15560  2sqlem8  15571  nninfsellemeqinf  15915  nninffeq  15919  nnnninfex  15921  exmidsbthrlem  15923  cvgcmp2nlemabs  15933