Theorem eqidd 2194

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

Syntax hints:   -> wi 4   = wceq 1364

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 1460  ax-ext 2175

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

This theorem is referenced by:  cbvraldva  2735  cbvrexdva  2736  rspcedeq1vd  2874  rspcedeq2vd  2875  nelrdva  2968  opeq2  3806  mpteq1  4114  tfisi  4620  feq23d  5400  fvmptdv2  5648  elrnrexdm  5698  fmptco  5725  cofmpt  5728  ftpg  5743  fliftfun  5840  fliftval  5844  cbvmpo  5998  fconstmpo  6014  eqfnov2  6027  ovmpod  6047  ovmpodv2  6053  fvmpopr2d  6056  elovmporab  6120  elovmporab1w  6121  ofvalg  6142  ofrval  6143  off  6145  ofres  6147  suppssof1  6150  ofco  6151  caofref  6156  caofrss  6159  caoftrn  6160  uchoice  6192  rdgivallem  6436  iserd  6615  ixpsnf1o  6792  1domsn  6875  mapxpen  6906  infnninf  7185  ctssexmid  7211  nninfdcinf  7232  nninfwlporlemd  7233  nninfwlporlem  7234  nninfwlpoimlemginf  7237  ofnegsub  8983  infrenegsupex  9662  fz0to4untppr  10193  fzo0to3tp  10289  modqsubmod  10456  0tonninf  10514  iseqovex  10532  seqvalcd  10535  seq3f1olemqsumkj  10585  seq3id  10599  seq3id2  10600  resqrexlemp1rp  11153  resqrexlemfp1  11156  resqrex  11173  infxrnegsupex  11409  climcl  11428  clim2  11429  climuni  11439  climeq  11445  2clim  11447  climshftlemg  11448  climabs0  11453  climcn1  11454  climcn2  11455  climge0  11471  climsqz  11481  climsqz2  11482  climcau  11493  climrecvg1n  11494  climcaucn  11497  serf0  11498  isumz  11535  fisumss  11538  fsumsplitsn  11556  fsumsplitsnun  11565  isumclim3  11569  isummulc2  11572  fsum2dlemstep  11580  fsumconst  11600  fsumabs  11611  fsumparts  11616  iserabs  11621  fsumiun  11623  isumshft  11636  cvgratnnlemseq  11672  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  prod1dc  11732  fprodssdc  11736  fprodunsn  11750  fprodcl2lem  11751  fprodconst  11766  fprod2dlemstep  11768  fprodsplitsn  11779  eftlcl  11834  reeftlcl  11835  eftlub  11836  efsep  11837  effsumlt  11838  eirraplem  11923  2tp1odd  12028  bezoutlemstep  12137  nninfctlemfo  12180  alginv  12188  algfx  12193  cncongr1  12244  qnumdencoprm  12334  qeqnumdivden  12335  ctiunctal  12601  unct  12602  nninfdclemcl  12608  nninfdclemf  12609  nninfdclemp1  12610  nninfdc  12613  ressbasid  12691  ressressg  12696  prdsex  12883  imasex  12891  imasbas  12893  imasplusg  12894  imasmulr  12895  qusin  12912  igsumvalx  12975  gsumfzval  12977  gsumpropd  12978  gsumpropd2  12979  gsum0g  12982  gsumval2  12983  issgrp  12989  sgrp1  12997  issgrpd  12998  ismndd  13021  mndprop  13025  ress0g  13027  insubm  13060  resmhm  13062  resmhm2  13063  resmhm2b  13064  gsumfzz  13070  grpprop  13093  grpsubfvalg  13120  grpressid  13136  grpsubpropdg  13179  imasgrp2  13183  imasgrp  13184  imasgrpf1  13185  mulgfvalg  13194  mulgnngsum  13200  mulgpropdg  13237  submmulg  13239  subginv  13254  subgcl  13257  subgsub  13259  releqgg  13293  eqgex  13294  eqgfval  13295  qusgrp  13305  resghm  13333  ablprop  13370  subcmnd  13406  ablressid  13408  gsumfzmptfidmadd  13412  gsumfzconst  13414  gsumfzconstf  13415  gsumfzmhm2  13417  isrng  13433  isrngd  13452  rngressid  13453  imasrng  13455  issrg  13464  srgidmlem  13477  isring  13499  ringass  13515  ringidmlem  13521  ringabl  13531  ringprop  13539  isringd  13540  ring1  13558  ringressid  13562  imasring  13563  opprrng  13576  opprring  13578  opprringbg  13579  opprsubgg  13583  mulgass3  13584  dvdsrcld  13596  dvdsrex  13597  dvdsrcl2  13598  dvdsrid  13599  dvdsrtr  13600  dvdsrneg  13602  dvdsr01  13603  1unit  13606  unitcld  13607  opprunitd  13609  crngunit  13610  unitmulcl  13612  unitgrpbasd  13614  unitgrp  13615  unitabl  13616  unitgrpid  13617  unitsubm  13618  unitlinv  13625  unitrinv  13626  unitnegcl  13629  dvrfvald  13632  dvrvald  13633  dvrcl  13634  unitdvcl  13635  dvrid  13636  dvr1  13637  dvrdir  13642  rdivmuldivd  13643  dvdsrpropdg  13646  unitpropdg  13647  invrpropdg  13648  rhmf1o  13667  rhmdvdsr  13674  elrhmunit  13676  rhmunitinv  13677  issubrng2  13709  subrngpropd  13715  subrgcrng  13724  subrgdvds  13734  subrguss  13735  subrginv  13736  subrgdv  13737  subrgunit  13738  subrgugrp  13739  issubrg2  13740  subrgpropd  13752  aprirr  13782  aprsym  13783  aprcotr  13784  aprap  13785  islmodd  13792  lmodabl  13833  lss1  13861  lsssn0  13869  islss3  13878  lss1d  13882  lssintclm  13883  lsslsp  13928  sralmod  13949  sralmod0g  13950  rlmfn  13952  rlmvalg  13953  rlm0g  13956  rlmvnegg  13964  lidlssbas  13976  islidlm  13978  rnglidlmsgrp  13996  rnglidlrng  13997  qus2idrng  14024  crngridl  14029  quscrng  14032  cnfldui  14088  dvdsrzring  14102  zrhpropd  14125  znzrh  14142  znbas  14143  zncrng  14144  znzrhfo  14147  znf1o  14150  znunit  14158  psrval  14163  psrbaglesuppg  14169  psrbasg  14170  psrplusgg  14173  epttop  14269  lmss  14425  txlm  14458  lmcn2  14459  cnmpt2c  14469  txswaphmeolem  14499  blfvalps  14564  bdxmet  14680  mpomulcn  14745  fsumcncntop  14746  cncfmptc  14775  cncfmpt1f  14777  cdivcncfap  14783  negfcncf  14785  divcncfap  14793  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dviaddf  14884  dvexp  14890  dvmptaddx  14898  dvmptmulx  14899  dvmptfsum  14904  dvef  14906  elply2  14914  elplyr  14919  plyaddlem1  14926  plycolemc  14936  sincn  14945  coscn  14946  lgsdir2lem5  15189  gausslemma2dlem1  15218  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgsquad2lem2  15239  2lgslem1b  15246  2lgslem3b1  15255  2lgslem3c1  15256  2lgsoddprmlem4  15269  2sqlem8  15280  nninfsellemeqinf  15576  nninffeq  15580  exmidsbthrlem  15582  cvgcmp2nlemabs  15592