Theorem eqidd 2082

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

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  cbvraldva  2583  cbvrexdva  2584  rspcedeq1vd  2709  rspcedeq2vd  2710  nelrdva  2797  opeq2  3571  mpteq1  3862  tfisi  4328  feq23d  5062  fvmptdv2  5281  elrnrexdm  5327  fmptco  5351  ftpg  5368  fliftfun  5456  fliftval  5460  cbvmpt2  5603  eqfnov2  5628  ovmpt2d  5648  ovmpt2dv2  5654  fnofval  5741  ofrval  5742  off  5744  ofres  5745  suppssof1  5748  ofco  5749  caofref  5752  caofrss  5755  caoftrn  5756  rdgivallem  5991  iserd  6155  infrenegsupex  8682  fzo0to3tp  9228  modqsubmod  9384  iseqovex  9439  iseqid  9467  resqrexlemp1rp  9892  resqrexlemfp1  9895  resqrex  9912  climcl  10121  clim2  10122  climuni  10132  climeq  10138  2clim  10140  climshftlemg  10141  climabs0  10146  climcn1  10147  climcn2  10148  climge0  10163  climsqz  10173  climsqz2  10174  climcau  10184  climrecvg1n  10185  climcaucn  10188  serif0  10189  2tp1odd  10284  bezoutlemstep  10386  ialginv  10429  ialgfx  10434  cncongr1  10485