Theorem eqidd 2178

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

Syntax hints:   -> wi 4   = wceq 1353

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 1449  ax-ext 2159

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

This theorem is referenced by:  cbvraldva  2712  cbvrexdva  2713  rspcedeq1vd  2850  rspcedeq2vd  2851  nelrdva  2944  opeq2  3778  mpteq1  4085  tfisi  4584  feq23d  5358  fvmptdv2  5602  elrnrexdm  5652  fmptco  5679  cofmpt  5682  ftpg  5697  fliftfun  5792  fliftval  5796  cbvmpo  5949  fconstmpo  5965  eqfnov2  5977  ovmpod  5997  ovmpodv2  6003  ofvalg  6087  ofrval  6088  off  6090  ofres  6092  suppssof1  6095  ofco  6096  caofref  6099  caofrss  6102  caoftrn  6103  rdgivallem  6377  iserd  6556  ixpsnf1o  6731  1domsn  6814  mapxpen  6843  infnninf  7117  ctssexmid  7143  nninfdcinf  7164  nninfwlporlemd  7165  nninfwlporlem  7166  nninfwlpoimlemginf  7169  infrenegsupex  9588  fz0to4untppr  10117  fzo0to3tp  10212  modqsubmod  10375  0tonninf  10432  iseqovex  10449  seqvalcd  10452  seq3f1olemqsumkj  10491  seq3id  10501  seq3id2  10502  resqrexlemp1rp  11006  resqrexlemfp1  11009  resqrex  11026  infxrnegsupex  11262  climcl  11281  clim2  11282  climuni  11292  climeq  11298  2clim  11300  climshftlemg  11301  climabs0  11306  climcn1  11307  climcn2  11308  climge0  11324  climsqz  11334  climsqz2  11335  climcau  11346  climrecvg1n  11347  climcaucn  11350  serf0  11351  isumz  11388  fisumss  11391  fsumsplitsn  11409  fsumsplitsnun  11418  isumclim3  11422  isummulc2  11425  fsum2dlemstep  11433  fsumconst  11453  fsumabs  11464  fsumparts  11469  iserabs  11474  fsumiun  11476  isumshft  11489  cvgratnnlemseq  11525  mertenslemub  11533  mertenslemi1  11534  mertenslem2  11535  prod1dc  11585  fprodssdc  11589  fprodunsn  11603  fprodcl2lem  11604  fprodconst  11619  fprod2dlemstep  11621  fprodsplitsn  11632  eftlcl  11687  reeftlcl  11688  eftlub  11689  efsep  11690  effsumlt  11691  eirraplem  11775  2tp1odd  11879  bezoutlemstep  11988  alginv  12037  algfx  12042  cncongr1  12093  qnumdencoprm  12183  qeqnumdivden  12184  ctiunctal  12432  unct  12433  nninfdclemcl  12439  nninfdclemf  12440  nninfdclemp1  12441  nninfdc  12444  ressressg  12524  issgrp  12739  sgrp1  12746  ismndd  12768  mndprop  12772  insubm  12800  grpprop  12822  grpsubfvalg  12846  grpressid  12859  grpsubpropdg  12902  mulgfvalg  12913  mulgpropdg  12952  subginv  12967  subgcl  12970  subgsub  12972  ablprop  13000  subcmnd  13029  issrg  13048  srgidmlem  13061  isring  13083  ringass  13099  ringidmlem  13105  ringabl  13115  ringprop  13119  isringd  13120  ring1  13136  opprring  13148  opprringbg  13149  mulgass3  13153  dvdsrcld  13165  dvdsrex  13166  dvdsrcl2  13167  dvdsrid  13168  dvdsrtr  13169  dvdsrneg  13171  dvdsr01  13172  1unit  13175  unitcld  13176  opprunitd  13178  crngunit  13179  unitmulcl  13181  unitgrpbasd  13183  unitgrp  13184  unitabl  13185  unitgrpid  13186  unitsubm  13187  unitlinv  13194  unitrinv  13195  unitnegcl  13198  dvrfvald  13201  dvrvald  13202  dvrcl  13203  unitdvcl  13204  dvrid  13205  dvr1  13206  dvrdir  13211  rdivmuldivd  13212  dvdsrpropdg  13215  unitpropdg  13216  invrpropdg  13217  aprirr  13240  aprsym  13241  aprcotr  13242  aprap  13243  epttop  13372  lmss  13528  txlm  13561  lmcn2  13562  cnmpt2c  13572  txswaphmeolem  13602  blfvalps  13667  bdxmet  13783  fsumcncntop  13838  cncfmptc  13864  cncfmpt1f  13866  cdivcncfap  13869  negfcncf  13871  dvidlemap  13942  dvcnp2cntop  13945  dvaddxxbr  13947  dvmulxxbr  13948  dviaddf  13951  dvexp  13957  dvmptaddx  13963  dvmptmulx  13964  dvef  13970  sincn  13972  coscn  13973  lgsdir2lem5  14215  2sqlem8  14241  nninfsellemeqinf  14536  nninffeq  14540  exmidsbthrlem  14541  cvgcmp2nlemabs  14551