Theorem eqidd 2038

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	⊢ (φ → A = A)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2037	. 2 ⊢ A = A
2	1	a1i 9	1 ⊢ (φ → A = A)

Syntax hints:   → wi 4   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1335  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  cbvraldva  2533  cbvrexdva  2534  nelrdva  2740  opeq2  3541  mpteq1  3832  tfisi  4253  feq23d  4985  fvmptdv2  5203  elrnrexdm  5249  fmptco  5273  ftpg  5290  fliftfun  5379  fliftval  5383  cbvmpt2  5525  eqfnov2  5550  ovmpt2d  5570  ovmpt2dv2  5576  fnofval  5663  ofrval  5664  off  5666  ofres  5667  suppssof1  5670  ofco  5671  caofref  5674  caofrss  5677  caoftrn  5678  rdgivallem  5908  iserd  6068  fzo0to3tp  8845  iseqovex  8899